remove examples and instances

theories/examples/counterexamples.v

-From iris.algebra Require Import base stepindex.
-
-(** counter-examples for existential properties *)
-Section existential_negative.
-  (* Transfinite step-index types cannot validate the bounded existential property. *)
-  Context {SI : indexT}. 
-  Record sProp := 
-    { 
-      prop : SI → Prop; 
-      prop_downclosed : ∀ α β, α ≺ β → prop β → prop α
-    }. 
-  Program Definition sProp_later (P : sProp) := Build_sProp (λ γ, ∀ γ', γ' ≺ γ → prop P γ') _.
-  Next Obligation. 
-    intros [P Pdown] α β Hα. cbn. eauto with index.
-  Qed.
-  Program Definition sProp_false := Build_sProp (λ _, False) _. 
-  Next Obligation.  intros. assumption. Qed.
-
-  Program Definition sProp_ex {X} (Φ : X → sProp) := Build_sProp (λ α, ∃ x, prop (Φ x) α) _. 
-  Next Obligation. 
-    intros X Φ α β Hα. cbn. intros [x H]. exists x. by eapply prop_downclosed. 
-  Qed.
-
-  Definition bounded_existential (X : Type) (Φ : X → sProp) α:=
-    (∀ β, β ≺ α → ∃ x : X, prop (Φ x) β)
-    → ∃ x : X, ∀ β, β ≺ α → prop (Φ x) β.
-  Definition existential (X : Type) (Φ : X → sProp) := 
-    (∀ α, ∃ x : X, prop (Φ x) α) 
-    → ∃ x : X, ∀ α, prop (Φ x) α. 
-
-  Section transfinite.
-    Hypothesis (ω: SI).
-    Hypothesis (is_limit_of_nat: ∀ n, Nat.iter n (index_succ SI) zero ≺ ω).
-    Hypothesis (is_smallest: ∀ α, α ≺ ω → ∃ n, α = Nat.iter n (index_succ SI) zero).
-    
-    Lemma transfinite_no_bounded_existential : 
-      bounded_existential nat (λ n, Nat.iter n sProp_later sProp_false) ω → False.
-    Proof. 
-      intros H. unfold bounded_existential in H. edestruct H as [n H']. 
-      { intros β Hβ. apply is_smallest in Hβ as (n & ->). exists (S n).
-        induction n as [ | n IH]. 
-        - intros ? []%index_lt_zero_is_normal.
-        - intros α Hα. apply index_succ_iff in Hα as [ -> | Hα]. now apply IH. 
-          intros β Hβ. apply IH. eauto with index. 
-      } 
-      specialize (H' (Nat.iter n (index_succ SI) zero) ltac:(apply is_limit_of_nat)). 
-      induction n as [ | n IH]; cbn in H'. exact H'. 
-      apply IH. apply H'. apply index_succ_greater. 
-    Qed.
-  End transfinite.
-End existential_negative.
-
-Section no_later_exists.
-(** A step-indexed logic cannot have 
-  * a sound later-operation,  
-  * Löb induction 
-  * Commutation of later with existentials: ▷ (∃ x. P) ⊢ ▷ False ∨ ∃ x. ▷ P
-  * the existential property for countable types, if ⊢ ∃ n : nat. P n, then there is n : nat such that ⊢ P n. 
-*)
-
-  Context 
-    (PROP : Type) (* the type of propositions *)
-    (entail : PROP → PROP → Prop) (* the entailment relation *)
-    (TRUE : PROP) (* the true proposition *)
-    (FALSE : PROP) (* the false proposition *)
-    (later : PROP → PROP) (* the later modality *)
-    (ex : (nat → PROP) → PROP). (* for simplicity, we restrict to predicates over nat here since we don't need more for the proof *)
-
-  Implicit Types (P Q: PROP). 
-
-  Notation "▷ P" := (later P) (at level 20). 
-  Notation "P ⊢ Q" := (entail P Q) (at level 60). 
-  Notation "⊢ P" := (entail TRUE P) (at level 60). 
-
-  (* standard structural rules *)
-  Context 
-    (cut : ∀ P Q R, P ⊢ Q → Q ⊢ R → P ⊢ R)
-    (assumption : ∀ P, P ⊢ P)
-    (ex_intro : ∀ P Φ, (∃ n, P ⊢ Φ n) → P ⊢ ex Φ)
-    (ex_elim : ∀ P Φ, (∀ n, Φ n ⊢ P) → ex Φ ⊢ P). 
-
-  
-  (* relevant assumptions about our step-indexed logic *)
-  Context 
-    (logic_sound: ¬ ⊢ FALSE) 
-    (later_sound: ∀ P, ⊢ ▷ P → ⊢ P) (* later is sound *)
-    (existential : ∀ (Φ : nat → PROP), (⊢ ex Φ) → ∃ n, ⊢ (Φ n)) (* the existential property for nat *)
-    (Löb : ∀ P, (▷ P ⊢ P) → ⊢ P). (* Löb induction *)
-    
-  (* now later commuting with existentials is contradictory *)
-  Lemma no_later_existential_commuting : 
-    (∀ Φ, ▷ (ex Φ) ⊢ (ex (λ n, ▷ (Φ n))) )
-    → False.
-  Proof. 
-    intros Hcomm. apply logic_sound.  
-    assert (∃ n, ⊢ Nat.iter n later FALSE) as [ n Hf]. 
-    { apply existential. 
-      apply Löb. 
-      eapply cut. apply Hcomm. 
-      apply ex_elim. 
-      intros n. apply ex_intro. exists (S n). apply assumption. 
-    } 
-    induction n as [ | n IH]. 
-    exact Hf. 
-    apply IH. apply later_sound, Hf. 
-  Qed.
-End no_later_exists.
-
-
-From iris.algebra Require Export cmra updates.
-From iris.base_logic Require Import upred. 
-From iris.bi Require Import notation.
-Section more_counterexamples. 
-  Context {I: indexT} {M : ucmraT I}.
-  Implicit Types φ : Prop.
-  Implicit Types P Q : uPred M.
-  Implicit Types A : Type.
-  Arguments uPred_holds {_ _} !_ _ _ /.
-  Hint Immediate uPred_in_entails : core.
-
-  Notation "P ⊢ Q" := (@uPred_entails I M P%I Q%I) : stdpp_scope.
-  Notation "(⊢)" := (@uPred_entails I M) (only parsing) : stdpp_scope.
-  Notation "P ⊣⊢ Q" := (@uPred_equiv I M P%I Q%I) : stdpp_scope.
-  Notation "(⊣⊢)" := (@uPred_equiv I M) (only parsing) : stdpp_scope.
-
-  Notation "'True'" := (uPred_pure True) : bi_scope.
-  Notation "'False'" := (uPred_pure False) : bi_scope.
-  Notation "'⌜' φ '⌝'" := (uPred_pure φ%type%stdpp) : bi_scope.
-  Infix "∧" := uPred_and : bi_scope.
-  Infix "∨" := uPred_or : bi_scope.
-  Infix "→" := uPred_impl : bi_scope.
-  Notation "∀ x .. y , P" :=
-    (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)) : bi_scope.
-  Notation "∃ x .. y , P" :=
-    (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)) : bi_scope.
-  Infix "∗" := uPred_sep : bi_scope.
-  Infix "-∗" := uPred_wand : bi_scope.
-  Notation "□ P" := (uPred_persistently P) : bi_scope.
-  Notation "■ P" := (uPred_plainly P) : bi_scope.
-  Notation "x ≡ y" := (uPred_internal_eq x y) : bi_scope.
-  Notation "▷ P" := (uPred_later P) : bi_scope.
-  Notation "|==> P" := (uPred_bupd P) : bi_scope.
-  Notation "▷^ n P" := (Nat.iter n uPred_later P) : bi_scope.
-  Notation "▷? p P" := (Nat.iter (Nat.b2n p) uPred_later P) : bi_scope.
-  Notation "⧍ P" := (∃ n, ▷^n P)%I : bi_scope.
-  Notation "⧍^ n P" := (Nat.iter n (λ Q, ⧍ Q) P)%I : bi_scope.
-
-  Import uPred_primitive. 
-
-  Section bounded_limit_preserving_counterexample.
-
-    Definition F (P: uPred M) : uPred M := P.
-    Definition G (P: uPred M) : uPred M := (∃ n, ▷^n False)%I.
-    Definition c {α: I} : bchain (uPredO M) α := bchain_const (∃ n, ▷^n False)%I α.
-
-    Hypothesis (omega: I).
-    Hypothesis (is_limit_of_nat: ∀ n, Nat.iter n (index_succ I) zero ≺ omega).
-    Hypothesis (is_smallest: ∀ α, α ≺ omega → ∃ n, α = Nat.iter n (index_succ I) zero).
-
-    Notation "'ω'" := omega.
-    Lemma zero_omega: zero ≺ ω.
-    Proof using I is_limit_of_nat omega. eapply (is_limit_of_nat 0). Qed.
-
-    Lemma bounded_limit_preserving_entails_counterexample:
-      ¬ BoundedLimitPreserving (λ P, F P ⊢ G P).
-    Proof using I M is_limit_of_nat is_smallest omega.
-      intros H. specialize (H ω zero_omega c); simpl in H.
-      assert (∀ β : I, β ≺ ω → F (⧍ ⌜False⌝) ⊢ G (⧍ ⌜False⌝)) as H'.
-      { intros ??. destruct (entails_po (I:=I) (M:=M)) as [R _]. apply R. }
-      specialize (H H'). destruct H as [H].
-      specialize (H ω ε (ucmra_unit_validN ω)).
-      unfold F in *. assert (bcompl zero_omega c ω ε) as H''.
-      { eapply bcompl_unfold. unfold c; simpl.
-        intros n' Hn' _ Hv. eapply is_smallest in Hn'.
-        destruct Hn' as [m ->]. unseal.
-        exists (S m). clear Hv H' H. induction m; cbn.
-        - intros ? [] % index_lt_zero_is_normal.
-        - intros n' Hn' n'' Hn''. eapply uPred_mono.
-          eapply IHm; eauto.
-          eapply index_lt_le_trans. eapply Hn''.
-          eapply index_succ_iff, Hn'.
-          all: eauto.
-      }
-      specialize (H H''). unfold G in *.
-      revert H; unseal. intros [n].
-      eapply uPred_mono with (n2 := (Nat.iter (S n) (index_succ I) zero)) in H; eauto.
-      clear H' H''. induction n; simpl in *; eauto.
-    Qed.
-
-  End bounded_limit_preserving_counterexample.
-
-  Section ne_does_not_preserve_limits.
-    (* we show that, in general, non-expansive maps do not preserve limits. *)
-
-    Program Definition f : uPredO M -n> uPredO M := λne P, (P ∧ ∃ n, ▷^n False)%I.
-    Next Obligation.
-      intros α x y Heq. apply and_ne. apply Heq. reflexivity.
-    Qed.
-    Definition c0 {α: I} : bchain (uPredO M) α := bchain_const (True)%I α.
-
-    Hypothesis (omega: I).
-    Hypothesis (is_limit_of_nat: ∀ n, Nat.iter n (index_succ I) zero ≺ omega).
-    Hypothesis (is_smallest: ∀ α, α ≺ omega → ∃ n, α = Nat.iter n (index_succ I) zero).
-
-
-    Notation "'ω'" := omega.
-    Lemma zero_omega': zero ≺ ω.
-    Proof using I is_limit_of_nat omega. eapply (is_limit_of_nat 0). Qed.
-
-    Lemma test : ¬ (f (bcompl zero_omega' c0) ≡ bcompl zero_omega' (bchain_map f c0)).
-    Proof using is_smallest.
-      intros Heq. destruct Heq as [Heq]. specialize (Heq omega ε (ucmra_unit_validN _)).
-      cbn in Heq. destruct Heq as [_ H1].
-      revert H1. rewrite !bcompl_unfold; cbn. unseal. intros H. destruct H as [ _ H].
-      2: { destruct H as [n H]. eapply uPred_mono with (n2 := Nat.iter (S n) (index_succ I) zero) in H; eauto.
-        induction n as [ | n IH]; cbn in H; [tauto | ].
-        eapply IH. apply H. eapply index_succ_greater.
-      }
-      intros. split; [easy | ]. apply is_smallest in Hn' as [nn ->]. exists (S nn).
-      clear H0 H. induction nn as [ | n IH]; cbn.
-      - intros ? []%index_lt_zero_is_normal.
-      - intros n' Hn' n'' Hn''. apply IH. eapply index_lt_le_trans.
-        exact Hn''. apply index_succ_iff, Hn'.
-    Qed.
-  End ne_does_not_preserve_limits.
-
-End more_counterexamples.

theories/examples/keyideas/generalized_simulations.v

-From iris.base_logic Require Export iprop satisfiable.
-From iris.bi Require Export fixpoint.
-From iris.proofmode Require Import tactics.
-
-
-Section simulations.
-
-  Context {SI} `{LargeIndex SI} {Σ: gFunctors SI}.
-
-
-  (* We assume a source and a target language *)
-  Variable (S T: Type) (src_step: S → S → Prop) (tgt_step: T → T → Prop).
-  Variable (V: Type) (val_to_tgt: V → T) (φ: V → S → Prop).
-  Variable (val_irred: ∀ v, ¬ ∃ t', tgt_step (val_to_tgt v) t') (val_inj: Inj eq eq val_to_tgt).
-
-
-  (* refinements *)
-  Definition gtpr (t: T) (s: S) :=
-    (∀ v, rtc tgt_step t (val_to_tgt v) → ∃ s', rtc src_step s s' ∧ φ v s') ∧
-    (ex_loop tgt_step t → ex_loop src_step s).
-
-
-  Notation "S *d T" := (prodO (leibnizO SI T) (leibnizO SI S)) (at level 60).
-  Definition gsim_pre (sim: ((S *d T) → iProp Σ)) : (S *d T) → iProp Σ :=
-    (λ '(t, s),
-      (∃ v, ⌜φ v s⌝ ∧ ⌜val_to_tgt v = t⌝) ∨
-      (∃ t', ⌜tgt_step t t'⌝) ∧
-      (∀ t', ⌜tgt_step t t'⌝ → sim (t', s) ∨ ∃ s', ⌜src_step s s'⌝ ∧ ▷ sim (t', s'))
-    )%I.
-
-  Instance gsim_pre_mono: BiMonoPred gsim_pre.
-  Proof.
-    split.
-    - intros Φ Ψ. iIntros "#H" ([t s]).
-      rewrite /gsim_pre.
-      iIntros "[Hsim|Hsim]"; eauto.
-      iRight. iDestruct "Hsim" as "[Hsteps Hsim]".
-      iSplit; eauto.
-      iIntros (t' Htgt). iDestruct ("Hsim" $! t' Htgt) as "[Hsim|Hsim]".
-      + iLeft. by iApply "H".
-      + iRight. iDestruct "Hsim" as (s' Hsrc) "Hsim".
-        iExists s'. iSplit; eauto. iNext. by iApply "H".
-    - intros Φ Hdist α [t s] [t' s'] [Heq1 Heq2]; simpl in *.
-      repeat f_equiv; eauto.
-  Qed.
-
-  Definition gsim := bi_least_fixpoint gsim_pre.
-
-  Lemma sim_unfold t s:
-    (gsim (t, s) ⊣⊢ (∃ v, ⌜φ v s⌝ ∧ ⌜val_to_tgt v = t⌝) ∨
-    (∃ t', ⌜tgt_step t t'⌝) ∧
-    (∀ t', ⌜tgt_step t t'⌝ → gsim (t', s) ∨ ∃ s', ⌜src_step s s'⌝ ∧ ▷ gsim (t', s')))%I.
-  Proof.
-    fold (gsim_pre gsim (t, s)). iSplit.
-    - iApply least_fixpoint_unfold_1.
-    - iApply least_fixpoint_unfold_2.
-  Qed.
-
-
-  Lemma satisfiable_pure ψ: satisfiable (⌜ψ⌝: iProp Σ)%I → ψ.
-  Proof.
-    intros Hsat. apply satisfiable_elim in Hsat; last apply _.
-    by apply uPred.pure_soundness in Hsat.
-  Qed.
-
-  (* result preserving *)
-  Lemma gsim_execute_tgt_step t s t':
-    tgt_step t t' → satisfiable (gsim (t, s)) → ∃ s', rtc src_step s s' ∧ satisfiable (gsim (t', s')).
-  Proof.
-    intros Hstep Hsat.
-    eapply satisfiable_mono with (Q := (∃ s', ⌜rtc src_step s s'⌝ ∧ ▷ gsim (t', s'))%I) in Hsat.
-    - eapply satisfiable_exists in Hsat as [s' Hsat].
-      exists s'. split.
-      + eapply satisfiable_pure, satisfiable_mono; eauto. iIntros "[$ _]".
-      + eapply satisfiable_later, satisfiable_mono; eauto. iIntros "[_ $]".
-    - iIntros "Hsim". rewrite sim_unfold. iDestruct "Hsim" as "[Hsim|[_ Hsim]]".
-     + iDestruct "Hsim" as (v) "[_ <-]". exfalso. naive_solver.
-     + iDestruct ("Hsim" $! t' Hstep) as "[Hsim|Hsim]".
-       * iExists s. iSplit; first by iPureIntro. by iNext.
-       * iDestruct "Hsim" as (s' Hstep') "Hsim". iExists s'. iSplit; eauto.
-          iPureIntro. by eapply rtc_l.
-   Qed.
-
-  Lemma sim_execute_tgt t s t':
-    rtc tgt_step t t' → satisfiable (gsim (t, s)) → ∃ s', rtc src_step s s' ∧ satisfiable (gsim (t', s')).
-  Proof.
-    induction 1 in s.
-    - intros Hsim. exists s. by split.
-    - intros Hsim. eapply gsim_execute_tgt_step in Hsim; last eauto.
-      destruct Hsim as [s' [Hsrc Hsat]].
-      destruct (IHrtc _ Hsat) as [s'' [Hsrc' Hsat']].
-      exists s''. split; auto. by transitivity s'.
-  Qed.
-
-
-  (* termination preserving *)
-  Lemma sim_execute_tgt_step t s:
-    ex_loop tgt_step t → satisfiable (gsim (t, s)) →  ∃ t' s', src_step s s' ∧ ex_loop tgt_step t' ∧ satisfiable (gsim (t', s')).
-  Proof.
-    intros Hsteps Hsat.
-    eapply satisfiable_mono with (Q := (∃ t' s', ⌜src_step s s'⌝ ∧ ⌜ex_loop tgt_step t'⌝ ∧ ▷ gsim (t', s'))%I) in Hsat; last first.
-    iPoseProof (@least_fixpoint_strong_ind _ _ _ gsim_pre _ (λ '(t, s), ⌜ex_loop tgt_step t⌝ → ∃ (t' : T) (s' : S), ⌜src_step s s'⌝ ∧ ⌜ex_loop tgt_step t'⌝ ∧ ▷ gsim (t', s'))%I) as "Hind".
-    { intros ? [t'' s''] [t' s'] [Heq1 Heq2]; repeat f_equiv; eauto. }
-    - iIntros "Hsim". iRevert (Hsteps). iRevert "Hsim". iSpecialize ("Hind" with "[]"); last iApply ("Hind" $! (t, s)).
-      clear Hsat t s. iModIntro. iIntros ([t s]). iIntros "Hsim" (Hloop).
-      rewrite /gsim_pre. iDestruct "Hsim" as "[Hsim|Hsim]".
-      + iDestruct "Hsim" as (v) "[_ %]".
-        destruct Hloop as [t t']; subst t. naive_solver.
-      + iDestruct "Hsim" as "[_ Hsim]".
-        inversion Hloop as [t'' t' Hstep Hloop']; subst t''.
-        iDestruct ("Hsim" $! t' Hstep) as "[Hsim|Hsim]".
-        * iDestruct "Hsim" as "[Hsim _]". by iSpecialize ("Hsim" $! Hloop').
-        * iDestruct "Hsim" as (s' Hstep') "Hsim".
-          iExists t', s'. repeat iSplit; eauto.
-          iNext. iDestruct "Hsim" as "[_ $]".
-    - eapply satisfiable_exists in Hsat as [t' Hsat].
-      eapply satisfiable_exists in Hsat as [s' Hsat].
-      exists t', s'. repeat split.
-      + eapply satisfiable_pure, satisfiable_mono; eauto. iIntros "($ & _ & _)".
-      + eapply satisfiable_pure, satisfiable_mono; eauto. iIntros "(_ & $ & _)".
-      + eapply satisfiable_later, satisfiable_mono; eauto. iIntros "(_ & _ & $)".
-  Qed.
-
-  Lemma sim_divergence t s:
-    ex_loop tgt_step t → satisfiable (gsim (t, s)) → ex_loop src_step s.
-  Proof.
-    revert t s. cofix IH. intros t s Hloop Hsat.
-    edestruct sim_execute_tgt_step as (t' & s' & Hsrc & Hloop' & Hsim); [eauto..|].
-    econstructor; eauto.
-  Qed.
-
-  Lemma sim_is_tpr t s: (⊢ gsim (t, s)) → gtpr t s.
-  Proof.
-    intros Hsim. split.
-    - apply satisfiable_intro in Hsim. intros v Hsteps.
-      eapply sim_execute_tgt in Hsteps as [s' [Hsteps' Hsat]]; eauto.
-      enough (φ v s') by eauto.
-      eapply satisfiable_pure, satisfiable_mono; eauto.
-      rewrite sim_unfold. iIntros "[H|[H _]]".
-      + iDestruct "H" as (v')  "[% H]". by iDestruct "H" as %->%val_inj.
-      + iDestruct "H" as (t') "%". exfalso. naive_solver.
-    - intros Hloop. eapply sim_divergence; eauto.
-      apply satisfiable_intro, Hsim.
-  Qed.
-
-End simulations.
-

theories/examples/keyideas/simulations.v

-From iris.base_logic Require Export iprop satisfiable.
-From iris.bi Require Export fixpoint.
-From iris.proofmode Require Import tactics.
-
-
-Section simulations.
-
-  Context {SI} `{LargeIndex SI} {Σ: gFunctors SI}.
-
-
-  (* We assume a source and a target language *)
-  Variable (S T: Type) (src_step: S → S → Prop) (tgt_step: T → T → Prop).
-  Variable (V: Type) (val_to_src: V → S) (val_to_tgt: V → T).
-  Variable (val_irred: ∀ v, ¬ ∃ t', tgt_step (val_to_tgt v) t') (val_inj: Inj eq eq val_to_tgt).
-
-
-  (* refinements *)
-  Definition rpr (t: T) (s: S) :=
-    (∀ v, rtc tgt_step t (val_to_tgt v) → rtc src_step s (val_to_src v)).
-
-  Definition tpr (t: T) (s: S) :=
-    (∀ v, rtc tgt_step t (val_to_tgt v) → rtc src_step s (val_to_src v)) ∧
-    (ex_loop tgt_step t → ex_loop src_step s).
-
-  Definition sim_pre (sim: (T -d> S -d> iProp Σ)) : T -d> S -d> iProp Σ :=
-    (λ t s,
-      (∃ v, ⌜val_to_src v = s⌝ ∧ ⌜val_to_tgt v = t⌝) ∨
-      (∃ t', ⌜tgt_step t t'⌝) ∧
-      (∀ t', ⌜tgt_step t t'⌝ → ∃ s', ⌜src_step s s'⌝ ∧ ▷ sim t' s')
-    )%I.
-
-  Instance sim_pre_contr: Contractive sim_pre.
-  Proof.
-    intros a sim sim' Heq. unfold sim_pre.
-    intros t s. do 8 f_equiv. apply bi.later_contractive.
-    intros ??. by apply Heq.
-  Qed.
-
-
-  Definition sim := fixpoint sim_pre.
-
-  Lemma sim_unfold':
-    sim ≡ sim_pre sim.
-  Proof. by rewrite {1}/sim fixpoint_unfold. Qed.
-
-  Lemma sim_unfold t s:
-    (sim t s ⊣⊢ ((∃ v, ⌜val_to_src v = s⌝ ∧ ⌜val_to_tgt v = t⌝) ∨
-    (∃ t', ⌜tgt_step t t'⌝) ∧
-    (∀ t', ⌜tgt_step t t'⌝ → ∃ s', ⌜src_step s s'⌝ ∧ ▷ sim t' s')))%I.
-  Proof. apply sim_unfold'. Qed.
-
-  Instance sim_plain t s: Plain (sim t s).
-  Proof.
-    unfold Plain. iRevert (t s). iLöb as "IH".
-    iIntros (t s); rewrite sim_unfold.
-    iIntros "[H1|[H1 H2]]".
-    - iLeft. iApply (plain with "H1").
-    - iRight. iSplit; first iApply (plain with "H1").
-      iIntros (t' Hstep). iDestruct ("H2" $! t' Hstep) as (s' Hstep') "Hsim".
-      iExists s'; iSplit; first (iApply plain; by iPureIntro).
-      iApply later_plainly_1. iNext. by iApply "IH".
-  Qed.
-
-  Lemma sim_valid_satisfiable t s: satisfiable (sim t s) ↔ ⊢ sim t s.
-  Proof.
-    split.
-    - intros ? % satisfiable_elim; eauto. apply _.
-    - by intros ? % satisfiable_intro.
-  Qed.
-
-
-  Lemma satisfiable_pure φ: satisfiable (⌜φ⌝: iProp Σ)%I → φ.
-  Proof.
-    intros Hsat. apply satisfiable_elim in Hsat; last apply _.
-    by apply uPred.pure_soundness in Hsat.
-  Qed.
-
-  (* result preserving *)
-  Lemma sim_execute_tgt_step t s t':
-    tgt_step t t' → satisfiable (sim t s) → ∃ s', src_step s s' ∧ satisfiable (sim t' s').
-  Proof.
-    intros Hstep Hsat.
-    eapply satisfiable_mono with (Q := (∃ s', ⌜src_step s s'⌝ ∧ ▷ sim t' s')%I) in Hsat.
-    - eapply satisfiable_exists in Hsat as [s' Hsat].
-      exists s'. split.
-      + eapply satisfiable_pure, satisfiable_mono; eauto. iIntros "[$ _]".
-      + eapply satisfiable_later, satisfiable_mono; eauto. iIntros "[_ $]".
-    - iIntros "Hsim". rewrite sim_unfold. iDestruct "Hsim" as "[Hsim|[_ Hsim]]".
-     + iDestruct "Hsim" as (v) "[<- <-]". exfalso. naive_solver.
-     + iApply ("Hsim" $! t' Hstep).
-   Qed.
-
-  Lemma sim_execute_tgt t s t':
-    rtc tgt_step t t' → satisfiable (sim t s) 
-    → ∃ s', rtc src_step s s' ∧ satisfiable (sim t' s').
-  Proof.
-    induction 1 in s.
-    - intros Hsim. exists s. by split.
-    - intros Hsim. eapply sim_execute_tgt_step in Hsim; eauto.
-      destruct Hsim as [s' [Hsrc Hsat]].
-      destruct (IHrtc _ Hsat) as [s'' [Hsrc' Hsat']].
-      exists s''. split; auto. by eapply rtc_l.
-  Qed.
-
-  (* Lemma 2.1 *)
-  Lemma sim_is_rpr t s: (⊢ sim t s) → rpr t s.
-  Proof.
-    intros Hsim % sim_valid_satisfiable v Hsteps.
-    eapply sim_execute_tgt in Hsteps as [s' [Hsteps' Hsat]]; eauto.
-    enough (s' = (val_to_src v)) as -> by eauto.
-    eapply satisfiable_pure, satisfiable_mono; eauto.
-    rewrite sim_unfold. iIntros "[H|[H _]]".
-    - iDestruct "H" as (v')  "[<- H]". by iDestruct "H" as %->%val_inj.
-    - iDestruct "H" as (t') "%". exfalso. naive_solver.
-  Qed.
-
-
-  (* Lemma 2.2 *)
-  Lemma sim_is_tpr t s: (⊢ sim t s) → tpr t s.
-  Proof.
-    intros Hsim. split.
-    - by apply sim_is_rpr.
-    - apply sim_valid_satisfiable in Hsim. revert t s Hsim.
-      cofix IH. intros t s Hsat. inversion 1 as [t'' t' Hstep Hloop]; subst t''.
-      destruct (sim_execute_tgt_step _ _ _ Hstep Hsat) as [s' [Hstep' Hsat']].
-      econstructor; eauto.
-  Qed.
-End simulations.
-

theories/examples/refinements/derived.v

-
-From iris.program_logic.refinement Require Export ref_weakestpre ref_adequacy seq_weakestpre.
-From iris.examples.refinements Require Export refinement.
-From iris.algebra Require Import auth.
-From iris.heap_lang Require Import proofmode notation.
-From iris.proofmode Require Import tactics.
-Set Default Proof Using "Type".
-
-
-(* We illustrate here how to derive the rules shown in the paper *)
-
-
-Section derived.
-  Context {SI: indexT} `{Σ: gFunctors SI} `{!rheapG Σ} `{!auth_sourceG Σ (natA SI)} `{!seqG Σ}.
-
-  Definition seq_rswp E e φ : iProp Σ := (na_own seqG_name E -∗ RSWP e at 0 ⟨⟨ v, na_own seqG_name E ∗ φ v ⟩⟩)%I.
-  Notation "⟨⟨ P ⟩ ⟩ e ⟨⟨ v , Q ⟩ ⟩" := (□ (P -∗ (seq_rswp ⊤ e (λ v, Q))))%I
-  (at level 20, P, e, Q at level 200, format "⟨⟨  P  ⟩ ⟩  e  ⟨⟨  v ,  Q  ⟩ ⟩") : stdpp_scope.
-  Notation "{{ P } } e {{ v , Q } }" := (□ (P -∗ SEQ e ⟨⟨ v, Q ⟩⟩))%I
-  (at level 20, P, e, Q at level 200, format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
-
-
-  Lemma Value (v: val): (⊢ {{True}} v {{w, ⌜v = w⌝}})%I.
-  Proof.
-    iIntros "!> _ $". by iApply rwp_value.
-  Qed.
-
-  Lemma Frame (e: expr) P R Q: ({{P}} e {{v, Q v}} ⊢ {{P ∗ R}} e {{v, Q v ∗ R}})%I.
-  Proof.
-    iIntros "#H !> [P $]". by iApply "H".
-  Qed.
-
-  Lemma Bind (e: expr) K P Q R:
-    ({{P}} e {{v, Q v}} ∗ (∀ v: val, ({{Q v}} fill K (Val v) {{w, R w}}))
-    ⊢ {{P}} fill K e {{v, R v}})%I.
-  Proof.
-    iIntros "[#H1 #H2] !> P Hna".
-    iApply rwp_bind. iSpecialize ("H1" with "P Hna").
-    iApply (rwp_strong_mono with "H1 []"); auto.
-    iIntros (v) "[Hna Q] !>". iApply ("H2" with "Q Hna").
-  Qed.
-
-  Lemma Löb (P : iPropI Σ) : (▷ P → P) ⊢ P.
-  Proof. iApply bi.löb. Qed.
-
-  Lemma TPPureT (e e': expr) P Q: pure_step e e' → ({{P}} e' {{v, Q v}} ⊢ ⟨⟨P⟩⟩ e ⟨⟨v, Q v⟩⟩)%I.
-  Proof.
-    iIntros (Hstep) "#H !> P Hna".
-    iApply (ref_lifting.rswp_pure_step_later _ _ _ _ _ True); [|done|by iApply ("H" with "P Hna")].
-    intros _. apply nsteps_once, Hstep.
-  Qed.
-
-  Lemma TPPureS (e e' et: expr) K P Q:
-    to_val et = None
-    → pure_step e e'
-    → (⟨⟨src (fill K e') ∗ P⟩⟩ et ⟨⟨v, Q v⟩⟩ ⊢ {{src (fill K e) ∗ ▷ P}} et {{v, Q v}})%I.
-  Proof.
-    iIntros (Hexp Hstep) "#H !> [Hsrc P] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc]"); first done; last first.
-    - iApply step_pure; last iApply "Hsrc". apply pure_step_ctx; last done. apply _.
-    - iIntros "Hsrc'". iApply rswp_do_step. iNext. iApply ("H" with "[$P $Hsrc'] Hna").
-  Qed.
-
-  Lemma TPStoreT l (v1 v2: val): (True ⊢ ⟨⟨l ↦ v1⟩⟩ #l <- v2 ⟨⟨w, ⌜w = #()⌝ ∗ l ↦ v2⟩⟩)%I.
-  Proof.
-    iIntros "_ !> Hl $". iApply (rswp_store with "[$Hl]").
-    by iIntros "$".
-  Qed.
-
-  Lemma TPStoreS (et: expr) l v1 v2 K P Q:
-    to_val et = None
-    → (⟨⟨P ∗ src (fill K (Val #())) ∗ l ↦s v2⟩⟩ et ⟨⟨v, Q v⟩⟩
-      ⊢ {{src (fill K (#l <- v2)) ∗ l ↦s v1 ∗ ▷ P}} et {{v, Q v}})%I.
-  Proof.
-    iIntros (Hexp) "#H !> [Hsrc [Hloc P]] Hna". iApply (rwp_take_step with "[P Hna] [Hsrc Hloc]"); first done; last first.
-    - iApply step_store. iFrame.
-    - iIntros "Hsrc'". iApply rswp_do_step. iNext. iApply ("H" with "[$P $Hsrc'] Hna").
-  Qed.
-
-  Lemma TPStutterT (e: expr) P Q: to_val e = None → (⟨⟨P⟩⟩ e ⟨⟨v, Q v⟩⟩ ⊢ {{P}} e {{v, Q v}})%I.
-  Proof.
-    iIntros (H) "#H !> P Hna". iApply rwp_no_step; first done.
-    by iApply ("H" with "P Hna").
-  Qed.
-
-  Lemma TPStutterSStore (et : expr) v1 v2 K l P Q : 
-    to_val et = None
-    → {{P ∗ src (fill K (Val #())) ∗ l ↦s v2}} et {{v, Q v}} 
-    ⊢ {{l ↦s v1 ∗ src (fill K (#l <- v2)) ∗ P}} et {{v, Q v}}. 
-  Proof. 
-    iIntros (Hv) "#H !> [Hloc [Hsrc P]] Hna". 
-    iApply (rwp_weaken with "[H Hna] [P Hloc Hsrc]"); first done.
-    - instantiate (1 := (P ∗ src (fill K #()) ∗ l ↦s v2)%I). 
-      iIntros "H1". iApply ("H" with "[H1] [Hna]"); done. 
-    - iApply src_update_mono. iSplitL "Hsrc Hloc". 
-      iApply step_store. by iFrame. 
-      iIntros "[H0 H1]". by iFrame.
-  Qed. 
-
-  Lemma TPStutterSPure (et es es' : expr) P Q : 
-    to_val et = None
-    → pure_step es es'
-    → {{ P ∗ src(es') }} et {{v, Q v}}
-      ⊢ {{ P ∗ src(es)}} et {{v, Q v}}.
-  Proof. 
-    iIntros (H0 H) "#H !> [P Hsrc] Hna".
-    iApply (rwp_weaken with "[H Hna] [P Hsrc]"); first done. 
-    - instantiate (1 := (P ∗ src es')%I). iIntros "H1". 
-      by iApply ("H" with "[H1] Hna"). 
-    - iApply src_update_mono. iSplitL "Hsrc". 
-      by iApply step_pure. iIntros "?"; by iFrame. 
-  Qed.  
-
-  Lemma HoareLöb X P Q e : 
-    (∀ x :X, {{P x ∗ ▷ (∀ x, {{P x}} e {{v, Q x v}})}} e {{ v, Q x v}})
-    ⊢ ∀ x, {{ P x }} e {{v, Q x v}}. 
-  Proof. 
-    iIntros "H". iApply bi.löb. 
-    iIntros "#H1" (x). 
-    (*iIntros "H0".*)
-    (*iSpecialize ("H" with x). *)
-    (*iApply ("H"). iModIntro.*)
-  Abort. 
-
-End derived.

theories/examples/safety/assert.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
-
-Definition assert : val :=
-  λ: "v", if: "v" #() then #() else #0 #0. (* #0 #0 is unsafe *)
-(* just below ;; *)
-Notation "'assert:' e" := (assert (λ: <>, e)%E) (at level 99) : expr_scope.
-Notation "'assert:' e" := (assert (λ: <>, e)%V) (at level 99) : val_scope.
-
-(*
-Lemma twp_assert `{!heapG Σ} E (Φ : val → iProp Σ) e :
-  WP e @ E [{ v, ⌜v = #true⌝ ∧ Φ #() }] -∗
-  WP (assert: e)%V @ E [{ Φ }].
-Proof.
-  iIntros "HΦ". wp_lam.
-  wp_apply (twp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
-Qed.*)
-
-Lemma wp_assert  {SI} {Σ: gFunctors SI} `{!heapG Σ} E (Φ : val → iProp Σ) e :
-  WP e @ E {{ v, ⌜v = #true⌝ ∧ ▷ Φ #() }} -∗
-  WP (assert: e)%V @ E {{ Φ }}.
-Proof.
-  iIntros "HΦ". wp_lam.
-  wp_apply (wp_wand with "HΦ"). iIntros (v) "[% ?]"; subst. by wp_if.
-Qed.

theories/examples/safety/barrier/barrier.v

-From iris.heap_lang Require Export notation.
-Set Default Proof Using "Type".
-
-Definition newbarrier : val := λ: <>, ref #false.
-Definition signal : val := λ: "x", "x" <- #true.
-Definition wait : val :=
-  rec: "wait" "x" := if: !"x" then #() else "wait" "x".

theories/examples/safety/barrier/example_client.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import adequacy proofmode.
-From iris.examples.safety Require Import par.
-From iris.examples.safety.barrier Require Import proof.
-Set Default Proof Using "Type".
-
-Definition worker (n : Z) : val :=
-  λ: "b" "y", wait "b" ;; !"y" #n.
-Definition client : expr :=
-  let: "y" := ref #0 in
-  let: "b" := newbarrier #() in
-  ("y" <- (λ: "z", "z" + #42) ;; signal "b") |||
-    (worker 12 "b" "y" ||| worker 17 "b" "y").
-
-Section client.
-  Local Set Default Proof Using "Type*".
-  Context `{Σ : gFunctors SI} `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
-
-  Definition N := nroot .@ "barrier".
-
-  Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
-    (∃ f : val, l ↦{q} f ∗ □ ∀ n : Z, WP f #n {{ v, ⌜v = #(n + 42)⌝ }})%I.
-
-  Lemma y_inv_split q l : y_inv q l -∗ (y_inv (q/2) l ∗ y_inv (q/2) l).
-  Proof.
-    iDestruct 1 as (f) "[[Hl1 Hl2] #Hf]".
-    iSplitL "Hl1"; iExists f; by iSplitL; try iAlways.
-  Qed.
-
-  Lemma worker_safe q (n : Z) (b y : loc) :
-    recv N b (y_inv q y) -∗ WP worker n #b #y {{ _, True }}.
-  Proof.
-    iIntros "Hrecv". wp_lam. wp_let.
-    wp_apply (wait_spec with "Hrecv"). iDestruct 1 as (f) "[Hy #Hf]".
-    wp_seq. wp_load.
-    iApply (wp_wand with "[]"). iApply "Hf". by iIntros (v) "_".
-  Qed.
-
-  Lemma client_safe : ⊢ WP client {{ _, True }}.
-  Proof.
-    iIntros ""; rewrite /client. wp_alloc y as "Hy". wp_let.
-    wp_apply (newbarrier_spec N (y_inv 1 y) with "[//]").
-    iIntros (l) "[Hr Hs]".
-    wp_apply (wp_par (λ _, True%I) (λ _, True%I) with "[Hy Hs] [Hr]"); last auto.
-    - (* The original thread, the sender. *)
-      wp_store. iApply (signal_spec with "[-]"); last by iNext; auto.
-      iSplitR "Hy"; first by eauto.
-      iExists _; iSplitL; [done|]. iIntros "!#" (n). by wp_pures.
-    - (* The two spawned threads, the waiters. *)
-      iDestruct (recv_weaken with "[] Hr") as "Hr".
-      { iIntros "Hy". by iApply (y_inv_split with "Hy"). }
-      iPoseProof (recv_split with "Hr") as "H". instantiate (1 := ⊤). done.
-      iApply swp_wp_lstep; eauto. 
-      iApply (lstepN_lstep _ _ 1). 
-      iMod "H". do 2 iModIntro. iNext. do 2 iModIntro. iMod "H". iModIntro. swp_finish. 
-      iDestruct "H" as "[H1 H2]".
-      wp_apply (wp_par (λ _, True%I) (λ _, True%I) with "[H1] [H2]"); last auto.
-      + by iApply worker_safe.
-      + by iApply worker_safe.
-Qed.
-End client.
-
-Section ClosedProofs.
-
-Let Σ {SI} : gFunctors SI := #[ heapΣ SI ; barrierΣ ; spawnΣ SI ].
-
-Lemma client_adequate {SI : indexT} σ : adequate NotStuck client σ (λ _ _, True).
-Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
-
-End ClosedProofs.
-
-(*Print Assumptions client_adequate.*)

theories/examples/safety/barrier/proof.v

-From iris.program_logic Require Export weakestpre.
-From iris.base_logic Require Import invariants saved_prop.
-From iris.heap_lang Require Export lang.
-From iris.heap_lang Require Import proofmode.
-From iris.algebra Require Import auth gset.
-From iris.examples.safety.barrier Require Export barrier.
-Set Default Proof Using "Type".
-
-(** The CMRAs/functors we need. *)
-Class barrierG {SI} (Σ : gFunctors SI) := BarrierG {
-  barrier_inG :> inG Σ (authR (gset_disjUR gname));
-  barrier_savedPropG :> savedPropG Σ;
-}.
-Definition barrierΣ {SI} : gFunctors SI :=
-  #[ GFunctor (authRF (gset_disjUR gname)); savedPropΣ ].
-
-Instance subG_barrierΣ `{Σ : gFunctors SI} : subG barrierΣ Σ → barrierG Σ.
-Proof. solve_inG. Qed.
-
-(** Now we come to the Iris part of the proof. *)
-Section proof.
-Context `{Σ : gFunctors SI} `{!heapG Σ, !barrierG Σ} (N : namespace).
-
-(* P is the proposition that will be sent, R the one that will be received by the individual threads *)
-Definition barrier_inv (l : loc) (γ : gname) (P : iProp Σ) : iProp Σ :=
-  (∃ (b : bool) (γsps : gset gname) (oracle : gname -> iProp Σ),
-    l ↦ #b ∗
-    own γ (● (GSet γsps)) ∗
-    ((if b then True else P) -∗ ▷ [∗ set] γsp ∈ γsps, oracle γsp) ∗
-    ([∗ set] γsp ∈ γsps, saved_prop_own γsp (oracle γsp)))%I.
-
-(*P is the proposition that will be sent, R' the one that will be received by this particular thread, and R the one we want to have *)
-Definition recv (l : loc) (R : iProp Σ) : iProp Σ :=
-  (∃ γ P R' γsp,
-    inv N (barrier_inv l γ P) ∗
-    ▷ (R' -∗ R) ∗
-    own γ (◯ GSet {[ γsp ]}) ∗
-    saved_prop_own γsp R')%I.
-
-(* P is the prop that we need to send *)
-Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
-  (∃ γ, inv N (barrier_inv l γ P))%I.
-
-(** Setoids *)
-Instance barrier_inv_ne l γ : NonExpansive (barrier_inv l γ).
-Proof. solve_proper. Qed.
-Global Instance send_ne l : NonExpansive (send l).
-Proof. solve_proper. Qed.
-Global Instance recv_ne l : NonExpansive (recv l).
-Proof. solve_proper. Qed.
-
-(** Actual proofs *)
-Lemma newbarrier_spec (P : iProp Σ) :
-  {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
-Proof.
-  iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam. wp_alloc l as "Hl".
-  iApply ("HΦ" with "[> -]").
-  iMod (saved_prop_alloc P) as (γsp) "#Hsp".
-  iMod (own_alloc (● GSet {[ γsp ]} ⋅ ◯ GSet {[ γsp ]})) as (γ) "[H● H◯]".
-  { by apply auth_both_valid. }
-  iMod (inv_alloc N _ (barrier_inv l γ P) with "[Hl H●]") as "#Hinv".
-  { iExists false, {[ γsp ]}, (fun _ => P). iIntros "{$Hl $H●} !>".
-    rewrite !big_sepS_singleton; eauto. }
-  iModIntro; iSplitL "H◯".
-  - iExists γ, P, P, γsp. iFrame; auto.
-  - by iExists γ.
-Qed.
-
-Lemma signal_spec l P :
-  {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}.
-Proof.
-  iIntros (Φ) "[Hs HP] HΦ".
-  iDestruct "Hs" as (γ) "#Hinv". wp_lam.
-  wp_swp. iInv "Hinv" as "H".
-  swp_last_step. iNext; simpl.
-  iDestruct "H" as ([] γsps oracle) "(Hl & H● & HRs & Hsaved)".
-  { wp_store. iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
-    iExists true, γsps, oracle. iFrame. }
-  wp_store. iDestruct ("HRs" with "HP") as "HRs".
-  iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
-  iExists true, γsps, oracle. iFrame; eauto.
-Qed.
-
-Lemma wait_spec l P:
-  {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
-Proof.
-  rename P into R.
-  iIntros (Φ) "HR HΦ".
-  iDestruct "HR" as (γ P R' γsp) "(#Hinv & HR & H◯ & #Hsp)".
-  iLöb as "IH". wp_rec. wp_bind (! _)%E.
-  iInv "Hinv" as "H". wp_swp. swp_step. iNext; simpl.
-  iDestruct "H" as ([] γsps oracle) "(Hl & H● & HRs & Hsaved)"; last first.
-  { wp_load. iModIntro. iSplitL "Hl H● HRs Hsaved".
-    { iExists false, γsps, oracle. iFrame. }
-    by wp_apply ("IH" with "[$] [$]"). }
-  iSpecialize ("HRs" with "[//]").
-  swp_last_step. iNext. wp_load.
-  iDestruct (own_valid_2 with "H● H◯")
-    as %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid.
-  iDestruct (big_sepS_delete with "HRs") as "[HR'' HRs]"; first done.
-  iDestruct (big_sepS_delete with "Hsaved") as "[HRsaved Hsaved]"; first done.
-  iDestruct (saved_prop_agree with "Hsp HRsaved") as "#Heq".
-  iMod (own_update_2 with "H● H◯") as "H●".
-  { apply (auth_update_dealloc _ _ (GSet (γsps ∖ {[ γsp ]}))).
-    apply gset_disj_dealloc_local_update. }
-  iIntros "!>". iSplitL "Hl H● HRs Hsaved".
-  { iModIntro.
-    iExists true, (γsps ∖ {[ γsp ]}), oracle. iFrame; eauto.
-  }
-  wp_if. iApply "HΦ". iApply "HR". by iRewrite "Heq".
-Qed.
-
-Lemma recv_split E l P1 P2 :
-  ↑N ⊆ E → ⊢ (recv l (P1 ∗ P2) -∗ |={E, ∅}=> ▷ |={∅, E}=> recv l P1 ∗ recv l P2)%I.
-Proof.
-  rename P1 into R1; rename P2 into R2.
-  iIntros (?). iDestruct 1 as (γ P R' γsp) "(#Hinv & HR & H◯ & #Hsp)".
-  iInv N as "H" "Hclose".
-  iMod (fupd_intro_mask' (E ∖ ↑N) ∅) as "H3". set_solver.
-  iModIntro. iNext.
-  iDestruct "H" as (b γsps oracle) "(Hl & H● & HRs & Hsaved)". (* as later does not commute with exists, this would fail without taking a step *)
-  iDestruct (own_valid_2 with "H● H◯")
-    as %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid.
-  set (γsps' := γsps ∖ {[γsp]}).
-  iMod (own_update_2 with "H● H◯") as "H●".
-  { apply (auth_update_dealloc _ _ (GSet γsps')).
-    apply gset_disj_dealloc_local_update. }
-  iMod (saved_prop_alloc_cofinite γsps' R1) as (γsp1 Hγsp1) "#Hsp1".
-  iMod (saved_prop_alloc_cofinite (γsps' ∪ {[ γsp1 ]}) R2)
-    as (γsp2 [? ?%not_elem_of_singleton]%not_elem_of_union) "#Hsp2".
-  iMod (own_update _ _ (● _ ⋅ (◯ GSet {[ γsp1 ]} ⋅ ◯ (GSet {[ γsp2 ]})))
-    with "H●") as "(H● & H◯1 & H◯2)".
-  { rewrite -auth_frag_op gset_disj_union; last set_solver.
-    apply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[ γsp1; γsp2 ]}).
-    set_solver. }
-  iMod "H3" as "_".
-  iMod ("Hclose" with "[HR Hl HRs Hsaved H●]") as "_".
-  { iModIntro. iExists b, ({[γsp1; γsp2]} ∪ γsps'),
-        (fun g => if (decide (g = γsp1)) then R1 else if (decide (g = γsp2)) then R2 else oracle g).
-    iIntros "{$Hl $H●}".
-    iDestruct (big_sepS_delete with "Hsaved") as "[HRsaved Hsaved]"; first done.
-    iSplitL "HR HRs HRsaved".
-    - iIntros "HP". iSpecialize ("HRs" with "HP").
-      iDestruct (saved_prop_agree with "Hsp HRsaved") as "#Heq".
-      iNext.
-      iDestruct (big_sepS_delete with "HRs") as "[HR'' HRs]"; first done.
-      iApply big_sepS_union; [set_solver|iSplitL "HR HR'' HRsaved"]; first last.
-      {
-        subst γsps'. iApply big_opS_forall. 2: iApply "HRs". cbn. intros γ' Hin.
-        destruct (decide (γ' = γsp1)) as [-> |_]. 1: by destruct Hγsp1.
-        destruct (decide (γ' = γsp2)) as [-> |_]. 1: by destruct H0.
-        reflexivity.
-      }
-      iApply big_sepS_union; [set_solver|].
-      iAssert (R')%I with "[HR'']" as "HR'"; [by iRewrite "Heq"|].
-      iDestruct ("HR" with "HR'") as "[HR1 HR2]".
-      iSplitL "HR1".
-      + iApply big_sepS_singleton. rewrite decide_True; done.
-      + iApply big_sepS_singleton. rewrite decide_False; [by rewrite decide_True | done].
-    - iApply big_sepS_union; [set_solver| iSplitR "Hsaved"]; first last.
-      {
-        subst γsps'. iApply big_opS_forall. 2: iApply "Hsaved". cbn. intros γ' Hin.
-        destruct (decide (γ' = γsp1)) as [-> | _]. by destruct Hγsp1.
-        destruct (decide (γ' = γsp2)) as [-> | _]. by destruct H0.
-        reflexivity.
-      }
-      iApply big_sepS_union; [set_solver|]; rewrite !big_sepS_singleton.
-      iSplitL.
-      + rewrite decide_True; done.
-      + rewrite decide_False; [by rewrite decide_True | done].
-  }
-  iModIntro; iSplitL "H◯1".
-  - iExists γ, P, R1, γsp1. iFrame; auto.
-  - iExists γ, P, R2, γsp2. iFrame; auto.
-Qed.
-
-Lemma recv_weaken l P1 P2 : (P1 -∗ P2) -∗ recv l P1 -∗ recv l P2.
-Proof.
-  iIntros "HP". iDestruct 1 as (γ P R' i) "(#Hinv & HR & H◯)".
-  iExists γ, P, R', i. iIntros "{$Hinv $H◯} !> HR'". iApply "HP". by iApply "HR".
-Qed.
-
-Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2.
-Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed.
-End proof.
-
-Typeclasses Opaque send recv.

theories/examples/safety/barrier/specification.v

-From iris.program_logic Require Export hoare.
-From iris.heap_lang Require Import proofmode.
-From iris.examples.safety.barrier Require Export barrier.
-From iris.examples.safety.barrier Require Import proof.
-Set Default Proof Using "Type".
-Import uPred.
-
-Section spec.
-Local Set Default Proof Using "Type*".
-Context `{Σ : gFunctors SI} `{!heapG Σ, !barrierG Σ}.
-
-Lemma barrier_spec (N : namespace) :
-  ∃ recv send : loc → iProp Σ -n> iProp Σ,
-    (∀ P, ⊢ {{ True }} newbarrier #()
-                     {{ v, ∃ l : loc, ⌜v = #l⌝ ∗ recv l P ∗ send l P }}) ∧
-    (∀ l P, ⊢ {{ send l P ∗ P }} signal #l {{ _, True }}) ∧
-    (∀ l P, ⊢ {{ recv l P }} wait #l {{ _, P }}) ∧
-    (∀ l P Q, recv l (P ∗ Q) -∗ |={↑N, ∅}=> ▷ |={∅, ↑N}=> recv l P ∗ recv l Q) ∧
-    (∀ l P Q, (P -∗ Q) -∗ recv l P -∗ recv l Q).
-Proof.
-  exists (λ l, OfeMor (recv N l)), (λ l, OfeMor (send N l)).
-  split_and?; simpl.
-  - iIntros (P) "!# _". iApply (newbarrier_spec _ P with "[]"); [done..|].
-    iNext. eauto.
-  - iIntros (l P) "!# [Hl HP]". iApply (signal_spec with "[$Hl $HP]"). by eauto.
-  - iIntros (l P) "!# Hl". iApply (wait_spec with "Hl"). eauto.
-  - iIntros (l P Q). by iApply recv_split.
-  - apply recv_weaken.
-Qed.
-End spec.

theories/examples/safety/clairvoyant_coin.v

-From iris.base_logic Require Export invariants.
-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang proofmode notation.
-From iris.examples.safety Require Export nondet_bool.
-
-(** The clairvoyant coin predicts all the values that it will
-*non-deterministically* choose throughout the execution of the
-program. This can be seen in the spec. The predicate [coin c bs]
-expresses that [bs] is the list of all the values of the coin in the
-future. The [read_coin] operation always returns the head of [bs] and the
-[toss_coin] operation takes the [tail] of [bs]. *)
-
-Definition new_coin: val :=
-  λ: <>, (ref (nondet_bool #()), NewProph).
-
-Definition read_coin : val := λ: "cp", !(Fst "cp").
-
-Definition toss_coin : val :=
-  λ: "cp",
-  let: "c" := Fst "cp" in
-  let: "p" := Snd "cp" in
-  let: "r" := nondet_bool #() in
-  "c" <- "r";; resolve_proph: "p" to: "r";; #().
-
-Section proof.
-  Context {SI} {Σ: gFunctors SI} `{!heapG Σ}.
-
-  Definition prophecy_to_list_bool (vs : list (val * val)) : list bool :=
-    (λ v, bool_decide (v = #true)) ∘ snd <$> vs.
-
-  Definition coin (cp : val) (bs : list bool) : iProp Σ :=
-    (∃ (c : loc) (p : proph_id) (vs : list (val * val)),
-        ⌜cp = (#c, #p)%V⌝ ∗
-        ⌜bs ≠ []⌝ ∗ ⌜tail bs = prophecy_to_list_bool vs⌝ ∗
-        proph p vs ∗
-        from_option (λ b : bool, c ↦ #b) (∃ b : bool, c ↦ #b) (head bs))%I.
-
-  Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c bs, RET c; coin c bs }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ".
-    wp_lam.
-    wp_apply wp_new_proph; first done.
-    iIntros (vs p) "Hp".
-    wp_apply nondet_bool_spec; first done.
-    iIntros (b) "_".
-    wp_alloc c as "Hc".
-    wp_pair.
-    iApply ("HΦ" $! (#c, #p)%V (b :: prophecy_to_list_bool vs)).
-    rewrite /coin; eauto with iFrame.
-  Qed.
-
-  Lemma read_coin_spec cp bs :
-    {{{ coin cp bs }}}
-      read_coin cp
-    {{{b bs', RET #b; ⌜bs = b :: bs'⌝ ∗ coin cp bs }}}.
-  Proof.
-    iIntros (Φ) "Hc HΦ".
-    iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
-    destruct bs as [|b bs]; simplify_eq/=.
-    wp_lam. wp_load.
-    iApply "HΦ"; iSplit; first done.
-    rewrite /coin; eauto 10 with iFrame.
-  Qed.
-
-  Lemma toss_coin_spec cp bs :
-    {{{ coin cp bs }}}
-      toss_coin cp
-    {{{b bs', RET #(); ⌜bs = b :: bs'⌝ ∗ coin cp bs' }}}.
-  Proof.
-    iIntros (Φ) "Hc HΦ".
-    iDestruct "Hc" as (c p vs -> ? ?) "[Hp Hb]".
-    destruct bs as [|b bs]; simplify_eq/=.
-    wp_lam. do 2 (wp_proj; wp_let).
-    wp_apply nondet_bool_spec; first done.
-    iIntros (r) "_".
-    wp_store.
-    wp_apply (wp_resolve_proph with "[Hp]"); first done.
-    iIntros (ws) "[-> Hp]".
-    wp_seq.
-    iApply "HΦ"; iSplit; first done.
-    destruct r; rewrite /coin; eauto 10 with iFrame.
-  Qed.
-
-End proof.

theories/examples/safety/counter.v

-From iris.program_logic Require Export weakestpre.
-From iris.base_logic.lib Require Export invariants.
-From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac_auth auth.
-From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
-
-Definition newcounter : val := λ: <>, ref #0.
-Definition incr : val := rec: "incr" "l" :=
-    let: "n" := !"l" in
-    if: CAS "l" "n" (#1 + "n") then #() else "incr" "l".
-Definition read : val := λ: "l", !"l".
-
-(** Monotone counter *)
-Class mcounterG {SI} (Σ: gFunctors SI) := MCounterG { mcounter_inG :> inG Σ (authR (mnatUR SI)) }.
-Definition mcounterΣ {SI} : gFunctors SI := #[GFunctor (authR (mnatUR SI))].
-
-Instance subG_mcounterΣ {SI} {Σ: gFunctors SI} : subG mcounterΣ Σ → mcounterG Σ.
-Proof. solve_inG. Qed.
-
-Section mono_proof.
-  Context {SI} {Σ: gFunctors SI} `{!heapG Σ, !mcounterG Σ} (N : namespace).
-
-  Definition mcounter_inv (γ : gname) (l : loc) : iProp Σ :=
-    (∃ n, own γ (● (n : mnat)) ∗ l ↦ #n)%I.
-
-  Definition mcounter (l : loc) (n : nat) : iProp Σ :=
-    (∃ γ, inv N (mcounter_inv γ l) ∧ own γ (◯ (n : mnat)))%I.
-
-  (** The main proofs. *)
-  Global Instance mcounter_persistent l n : Persistent (mcounter l n).
-  Proof. apply _. Qed.
-
-  Lemma newcounter_mono_spec :
-    {{{ True }}} newcounter #() {{{ l, RET #l; mcounter l 0 }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (● (O:mnat) ⋅ ◯ (O:mnat))) as (γ) "[Hγ Hγ']";
-      first by apply auth_both_valid.
-    iMod (inv_alloc N _ (mcounter_inv γ l) with "[Hl Hγ]").
-    { iNext. iExists 0%nat. by iFrame. }
-    iModIntro. iApply "HΦ". rewrite /mcounter; eauto 10.
-  Qed.
-
-  Lemma incr_mono_spec l n :
-    {{{ mcounter l n }}} incr #l {{{ RET #(); mcounter l (S n) }}}.
-  Proof.
-    iIntros (Φ) "Hl HΦ". iLöb as "IH". wp_rec.
-    iDestruct "Hl" as (γ) "[#? Hγf]".
-    wp_bind (! _)%E.
-    wp_swp 1%nat. iInv N as "H". swp_step. iNext. iDestruct "H" as (c) "[Hγ Hl]".
-    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures. wp_bind (CmpXchg _ _ _).
-   wp_swp 1%nat. iInv N as "H". swp_step. iNext. iDestruct "H" as (c') "[Hγ Hl]".
-    destruct (decide (c' = c)) as [->|].
-    - iDestruct (own_valid_2 with "Hγ Hγf")
-        as %[?%mnat_included _]%auth_both_valid.
-      iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply auth_update, (mnat_local_update _ _ (S c)); auto. }
-      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_pures. iApply "HΦ"; iExists γ; repeat iSplit; eauto.
-      iApply (own_mono with "Hγf").
-      (* FIXME: FIXME(Coq #6294): needs new unification *)
-      apply: auth_frag_mono. by apply mnat_included, le_n_S.
-    - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]). iModIntro.
-      iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_pures. iApply ("IH" with "[Hγf] [HΦ]"); last by auto.
-      rewrite {3}/mcounter; simpl; eauto 10.
-  Qed.
-
-  Lemma read_mono_spec l j :
-    {{{ mcounter l j }}} read #l {{{ i, RET #i; ⌜j ≤ i⌝%nat ∧ mcounter l i }}}.
-  Proof.
-    iIntros (ϕ) "Hc HΦ". iDestruct "Hc" as (γ) "[#Hinv Hγf]".
-    rewrite /read /=. wp_lam.
-    wp_swp 1%nat. iInv N as "H". swp_step. iNext. iDestruct "H" as (c) "[Hγ Hl]".
-    wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf")
-      as %[?%mnat_included _]%auth_both_valid.
-    iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-    { apply auth_update, (mnat_local_update _ _ c); auto. }
-    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    iApply ("HΦ" with "[-]"). rewrite /mcounter; simpl; eauto 10.
-  Qed.
-End mono_proof.
-
-(** Counter with contributions *)
-Class ccounterG {SI} Σ :=
-  CCounterG { ccounter_inG :> inG Σ (frac_authR (natR SI)) }.
-Definition ccounterΣ {SI} : gFunctors SI :=
-  #[GFunctor (frac_authR (natR SI))].
-
-Instance subG_ccounterΣ {SI} {Σ: gFunctors SI} : subG ccounterΣ Σ → ccounterG Σ.
-Proof. solve_inG. Qed.
-
-Section contrib_spec.
-  Context {SI} {Σ: gFunctors SI} `{!heapG Σ, !ccounterG Σ} (N : namespace).
-
-  Definition ccounter_inv (γ : gname) (l : loc) : iProp Σ :=
-    (∃ n, own γ (●F n) ∗ l ↦ #n)%I.
-
-  Definition ccounter_ctx (γ : gname) (l : loc) : iProp Σ :=
-    inv N (ccounter_inv γ l).
-
-  Definition ccounter (γ : gname) (q : frac) (n : nat) : iProp Σ :=
-    own γ (◯F{q} n).
-
-  (** The main proofs. *)
-  Lemma ccounter_op γ q1 q2 n1 n2 :
-    ccounter γ (q1 + q2) (n1 + n2) ⊣⊢ ccounter γ q1 n1 ∗ ccounter γ q2 n2.
-  Proof. by rewrite /ccounter frac_auth_frag_op -own_op. Qed.
-
-  Lemma newcounter_contrib_spec (R : iProp Σ) :
-    {{{ True }}} newcounter #()
-    {{{ γ l, RET #l; ccounter_ctx γ l ∗ ccounter γ 1 0 }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newcounter /=. wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (●F O%nat ⋅ ◯F 0%nat)) as (γ) "[Hγ Hγ']";
-      first by apply auth_both_valid.
-    iMod (inv_alloc N _ (ccounter_inv γ l) with "[Hl Hγ]").
-    { iNext. iExists 0%nat. by iFrame. }
-    iModIntro. iApply "HΦ". rewrite /ccounter_ctx /ccounter; eauto 10.
-  Qed.
-
-  Lemma incr_contrib_spec γ l q n :
-    {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} incr #l
-    {{{ RET #(); ccounter γ q (S n) }}}.
-  Proof.
-    iIntros (Φ) "[#? Hγf] HΦ". iLöb as "IH". wp_rec.
-    wp_bind (! _)%E.
-    wp_swp 1%nat. iInv N as "H". swp_step. iNext. iDestruct "H" as (c) "[Hγ Hl]".
-    wp_load. iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    wp_pures. wp_bind (CmpXchg _ _ _).
-    wp_swp 1%nat. iInv N as "H". swp_step. iNext. iDestruct "H" as (c') "[Hγ Hl]".
-    destruct (decide (c' = c)) as [->|].
-    - iMod (own_update_2 with "Hγ Hγf") as "[Hγ Hγf]".
-      { apply frac_auth_update, (nat_local_update _ _ (S c) (S n)); lia. }
-      wp_cmpxchg_suc. iModIntro. iSplitL "Hl Hγ".
-      { iNext. iExists (S c). rewrite Nat2Z.inj_succ Z.add_1_l. by iFrame. }
-      wp_pures. by iApply "HΦ".
-    - wp_cmpxchg_fail; first (by intros [= ?%Nat2Z.inj]).
-      iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c'; by iFrame|].
-      wp_pures. by iApply ("IH" with "[Hγf] [HΦ]"); auto.
-  Qed.
-
-  Lemma read_contrib_spec γ l q n :
-    {{{ ccounter_ctx γ l ∗ ccounter γ q n }}} read #l
-    {{{ c, RET #c; ⌜n ≤ c⌝%nat ∧ ccounter γ q n }}}.
-  Proof.
-    iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_lam.
-    wp_swp 1%nat. iInv N as "H". swp_step. iNext. iDestruct "H" as (c) "[Hγ Hl]".
-    wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf") as % ?%frac_auth_included_total%nat_included.
-    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    iApply ("HΦ" with "[-]"); rewrite /ccounter; simpl; eauto 10.
-  Qed.
-
-  Lemma read_contrib_spec_1 γ l n :
-    {{{ ccounter_ctx γ l ∗ ccounter γ 1 n }}} read #l
-    {{{ n, RET #n; ccounter γ 1 n }}}.
-  Proof.
-    iIntros (Φ) "[#? Hγf] HΦ".
-    rewrite /read /=. wp_lam.
-    wp_swp 1%nat. iInv N as "H". swp_step. iNext. iDestruct "H" as (c) "[Hγ Hl]".
-    wp_load.
-    iDestruct (own_valid_2 with "Hγ Hγf") as % <-%frac_auth_agreeL.
-    iModIntro. iSplitL "Hl Hγ"; [iNext; iExists c; by iFrame|].
-    by iApply "HΦ".
-  Qed.
-End contrib_spec.

theories/examples/safety/lazy_coin.v

-From iris.base_logic Require Export invariants.
-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang proofmode notation.
-From iris.examples.safety Require Export nondet_bool.
-
-Definition new_coin: val := λ: <>, (ref NONE, NewProph).
-
-Definition read_coin : val :=
-  λ: "cp",
-  let: "c" := Fst "cp" in
-  let: "p" := Snd "cp" in
-  match: !"c" with
-    NONE => let: "r" := nondet_bool #() in
-           "c" <- SOME "r";; resolve_proph: "p" to: "r";; "r"
-  | SOME "b" => "b"
-  end.
-
-Section proof.
-  Context {SI} {Σ: gFunctors SI} `{!heapG Σ}.
-
-  Definition val_to_bool (v : val) : bool := bool_decide (v = #true).
-
-  Definition prophecy_to_bool (vs : list (val * val)) : bool :=
-    default false (val_to_bool ∘ snd <$> head vs).
-
-  Lemma prophecy_to_bool_of_bool (b : bool) v vs :
-    prophecy_to_bool ((v, #b) :: vs) = b.
-  Proof. by destruct b. Qed.
-
-  Definition coin (cp : val) (b : bool) : iProp Σ :=
-    (∃ (c : loc) (p : proph_id) (vs : list (val * val)),
-        ⌜cp = (#c, #p)%V⌝ ∗ proph p vs ∗
-        (c ↦ SOMEV #b ∨ (c ↦ NONEV ∗ ⌜b = prophecy_to_bool vs⌝)))%I.
-
-  Lemma new_coin_spec : {{{ True }}} new_coin #() {{{ c b, RET c; coin c b }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ".
-    wp_lam.
-    wp_apply wp_new_proph; first done.
-    iIntros (vs p) "Hp".
-    wp_alloc c as "Hc".
-    wp_pair.
-    iApply ("HΦ" $! (#c, #p)%V ).
-    rewrite /coin; eauto 10 with iFrame.
-  Qed.
-
-  Lemma read_coin_spec cp b :
-    {{{ coin cp b }}} read_coin cp {{{ RET #b; coin cp b }}}.
-  Proof.
-    iIntros (Φ) "Hc HΦ".
-    iDestruct "Hc" as (c p vs ->) "[Hp [Hc | [Hc ->]]]".
-    - wp_lam. wp_load. wp_match.
-      iApply "HΦ".
-      rewrite /coin; eauto 10 with iFrame.
-    - wp_lam. wp_load. wp_match.
-      wp_apply nondet_bool_spec; first done.
-      iIntros (r) "_".
-      wp_let.
-      wp_store.
-      wp_apply (wp_resolve_proph with "[Hp]"); first done.
-      iIntros (ws) "[-> Hws]".
-      rewrite !prophecy_to_bool_of_bool.
-      wp_seq.
-      iApply "HΦ".
-      rewrite /coin; eauto with iFrame.
-  Qed.
-
-End proof.

theories/examples/safety/lock.v

-From iris.heap_lang Require Export lifting notation.
-From iris.base_logic.lib Require Export invariants.
-Set Default Proof Using "Type".
-
-Structure lock {SI} (Σ: gFunctors SI) `{!heapG Σ} := Lock {
-  (* -- operations -- *)
-  newlock : val;
-  acquire : val;
-  release : val;
-  (* -- predicates -- *)
-  (* name is used to associate locked with is_lock *)
-  name : Type;
-  is_lock (N: namespace) (γ: name) (lock: val) (R: iProp Σ) : iProp Σ;
-  locked (γ: name) : iProp Σ;
-  (* -- general properties -- *)
-  is_lock_ne N γ lk : NonExpansive (is_lock N γ lk);
-  is_lock_persistent N γ lk R : Persistent (is_lock N γ lk R);
-  locked_timeless γ : Timeless (locked γ);
-  locked_exclusive γ : locked γ -∗ locked γ -∗ False;
-  (* -- operation specs -- *)
-  newlock_spec N (R : iProp Σ) :
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock N γ lk R }}};
-  acquire_spec N γ lk R :
-    {{{ is_lock N γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}};
-  release_spec N γ lk R :
-    {{{ is_lock N γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}
-}.
-
-Arguments newlock {_ _ _} _.
-Arguments acquire {_ _ _} _.
-Arguments release {_ _ _} _.
-Arguments is_lock {_ _ _} _ _ _ _ _.
-Arguments locked {_ _ _} _ _.
-
-Existing Instances is_lock_ne is_lock_persistent locked_timeless.
-
-Instance is_lock_proper {SI} (Σ: gFunctors SI) `{!heapG Σ} (L: lock Σ) N γ lk:
-  Proper ((≡) ==> (≡)) (is_lock L N γ lk) := ne_proper _.
-

theories/examples/safety/nondet_bool.v

-From iris.base_logic Require Export invariants.
-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang proofmode notation.
-
-Definition nondet_bool : val :=
-  λ: <>, let: "l" := ref #true in Fork ("l" <- #false);; !"l".
-
-Section proof.
-  Context {SI} {Σ: gFunctors SI} `{!heapG Σ}.
-
-  Lemma nondet_bool_spec : {{{ True }}} nondet_bool #() {{{ (b : bool), RET #b; True }}}.
-  Proof.
-    iIntros (Φ) "_ HΦ".
-    wp_lam. wp_alloc l as "Hl". wp_let.
-    pose proof (nroot .@ "rnd") as rndN.
-    iMod (inv_alloc rndN _ (∃ (b : bool), l ↦ #b)%I with "[Hl]") as "#Hinv";
-      first by eauto.
-    wp_apply wp_fork.
-    - wp_swp 1%nat. iInv rndN as "H". swp_step. iNext. iDestruct "H" as (?) "?". wp_store; eauto.
-    - wp_seq. wp_swp 1%nat. iInv rndN as "H". swp_step. iNext. iDestruct "H" as (?) "?". wp_load.
-      iSplitR "HΦ"; first by eauto.
-      by iApply "HΦ".
-  Qed.
-
-End proof.

theories/examples/safety/par.v

-From iris.examples.safety Require Export spawn.
-From iris.heap_lang Require Import proofmode notation.
-Set Default Proof Using "Type".
-Import uPred.
-
-Definition parN : namespace := nroot .@ "par".
-
-Definition par : val :=
-  λ: "e1" "e2",
-    let: "handle" := spawn "e1" in
-    let: "v2" := "e2" #() in
-    let: "v1" := join "handle" in
-    ("v1", "v2").
-Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
-Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
-
-Section proof.
-Local Set Default Proof Using "Type*".
-Context {SI} {Σ: gFunctors SI} `{!heapG Σ, !spawnG Σ}.
-
-(* Notice that this allows us to strip a later *after* the two Ψ have been
-   brought together.  That is strictly stronger than first stripping a later
-   and then merging them, as demonstrated by [tests/joining_existentials.v].
-   This is why these are not Texan triples. *)
-Lemma par_spec (Ψ1 Ψ2 : val → iProp Σ) (f1 f2 : val) (Φ : val → iProp Σ) :
-  WP f1 #() {{ Ψ1 }} -∗ WP f2 #() {{ Ψ2 }} -∗
-  (▷ ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
-  WP par f1 f2 {{ Φ }}.
-Proof.
-  iIntros "Hf1 Hf2 HΦ". wp_lam. wp_let.
-  wp_apply (spawn_spec parN with "Hf1").
-  iIntros (l) "Hl". wp_let. wp_bind (f2 _).
-  wp_apply (wp_wand with "Hf2"); iIntros (v) "H2". wp_let.
-  wp_apply (join_spec with "[$Hl]"). iIntros (w) "H1".
-  iSpecialize ("HΦ" with "[$H1 $H2]"). by wp_pures.
-Qed.
-
-Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
-  WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
-  (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
-  WP (e1 ||| e2)%V {{ Φ }}.
-Proof.
-  iIntros "H1 H2 H".
-  wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
-Qed.
-End proof.

theories/examples/safety/spawn.v

-From iris.program_logic Require Export weakestpre.
-From iris.base_logic.lib Require Export invariants.
-From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl.
-Set Default Proof Using "Type".
-
-Definition spawn : val :=
-  λ: "f",
-    let: "c" := ref NONE in
-    Fork ("c" <- SOME ("f" #())) ;; "c".
-Definition join : val :=
-  rec: "join" "c" :=
-    match: !"c" with
-      SOME "x" => "x"
-    | NONE => "join" "c"
-    end.
-
-(** The CMRA & functor we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
-Class spawnG {SI} (Σ: gFunctors SI) := SpawnG { spawn_tokG :> inG Σ (exclR (unitO SI)) }.
-Definition spawnΣ SI : gFunctors SI := #[GFunctor (exclR (unitO SI))].
-
-Instance subG_spawnΣ {SI} {Σ: gFunctors SI} : subG (spawnΣ SI) Σ → spawnG Σ.
-Proof. solve_inG. Qed.
-
-(** Now we come to the Iris part of the proof. *)
-Section proof.
-Context {SI} {Σ: gFunctors SI} `{!heapG Σ, !spawnG Σ} (N : namespace).
-
-Definition spawn_inv (γ : gname) (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
-  (∃ lv, l ↦ lv ∗ (⌜lv = NONEV⌝ ∨
-                   ∃ w, ⌜lv = SOMEV w⌝ ∗ (Ψ w ∨ own γ (Excl ()))))%I.
-
-Definition join_handle (l : loc) (Ψ : val → iProp Σ) : iProp Σ :=
-  (∃ γ, own γ (Excl ()) ∗ inv N (spawn_inv γ l Ψ))%I.
-
-Global Instance spawn_inv_ne n γ l :
-  Proper (pointwise_relation val (dist n) ==> dist n) (spawn_inv γ l).
-Proof. solve_proper. Qed.
-Global Instance join_handle_ne n l :
-  Proper (pointwise_relation val (dist n) ==> dist n) (join_handle l).
-Proof. solve_proper. Qed.
-
-(** The main proofs. *)
-Lemma spawn_spec (Ψ : val → iProp Σ) (f : val) :
-  {{{ WP f #() {{ Ψ }} }}} spawn f {{{ l, RET #l; join_handle l Ψ }}}.
-Proof.
-  iIntros (Φ) "Hf HΦ". rewrite /spawn /=. wp_lam.
-  wp_alloc l as "Hl".
-  iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-  iMod (inv_alloc N _ (spawn_inv γ l Ψ) with "[Hl]") as "#?".
-  { iNext. iExists NONEV. iFrame; eauto. }
-  wp_apply (wp_fork with "[Hf]").
-  - iNext. wp_bind (f _). iApply (wp_wand with "Hf"); iIntros (v) "Hv".
-    wp_inj. iInv N as "H". wp_swp 1%nat. swp_step. iNext. iDestruct "H" as (v') "[Hl _]".
-    wp_store. iSplitL; last done. iIntros "!> !>". iExists (SOMEV v). iFrame. eauto.
-  - wp_pures. iApply "HΦ". rewrite /join_handle. eauto.
-Qed.
-
-Lemma join_spec (Ψ : val → iProp Σ) l :
-  {{{ join_handle l Ψ }}} join #l {{{ v, RET v; Ψ v }}}.
-Proof.
-  iIntros (Φ) "H HΦ". iDestruct "H" as (γ) "[Hγ #?]".
-  iLöb as "IH". wp_rec. wp_bind (! _)%E.
-  iInv N as "H". wp_swp 1%nat. swp_step. iNext. iDestruct "H" as (v) "[Hl Hinv]".
-  wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
-  - iModIntro. iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
-    wp_apply ("IH" with "Hγ [HΦ]"). auto.
-  - iDestruct "Hinv" as (v' ->) "[HΨ|Hγ']".
-    + iModIntro. iSplitL "Hl Hγ"; [iNext; iExists _; iFrame; eauto|].
-      wp_pures. by iApply "HΦ".
-    + iDestruct (own_valid_2 with "Hγ Hγ'") as %[].
-Qed.
-End proof.
-
-Typeclasses Opaque join_handle.

theories/examples/safety/spin_lock.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl.
-From iris.examples.safety Require Import lock.
-Set Default Proof Using "Type".
-
-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.
-
-(** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
-Class lockG {SI} (Σ: gFunctors SI) := LockG { lock_tokG :> inG Σ (exclR (unitO SI)) }.
-Definition lockΣ SI : gFunctors SI := #[GFunctor (exclR (unitO SI))].
-
-Instance subG_lockΣ {SI} {Σ: gFunctors SI} : subG (lockΣ SI) Σ → lockG Σ.
-Proof. solve_inG. Qed.
-
-Section proof.
-  Context {SI} {Σ: gFunctors SI} `{!heapG Σ, !lockG Σ} (N : namespace).
-
-  Definition lock_inv (γ : gname) (l : loc) (R : iProp Σ) : iProp Σ :=
-    (∃ b : bool, l ↦ #b ∗ if b then True else own γ (Excl ()) ∗ R)%I.
-
-  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
-    (∃ l: loc, ⌜lk = #l⌝ ∧ inv N (lock_inv γ l R))%I.
-
-  Definition locked (γ : gname) : iProp Σ := own γ (Excl ()).
-
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
-  Proof. iIntros "H1 H2". by iDestruct (own_valid_2 with "H1 H2") as %?. Qed.
-
-  Global Instance lock_inv_ne γ l : NonExpansive (lock_inv γ l).
-  Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γ l : NonExpansive (is_lock γ l).
-  Proof. solve_proper. Qed.
-
-  (** The main proofs. *)
-  Global Instance is_lock_persistent γ l R : Persistent (is_lock γ l R).
-  Proof. apply _. Qed.
-  Global Instance locked_timeless γ : Timeless (locked γ).
-  Proof. apply _. Qed.
-
-  Lemma newlock_spec (R : iProp Σ):
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
-  Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd /newlock /=.
-    wp_lam. wp_alloc l as "Hl".
-    iMod (own_alloc (Excl ())) as (γ) "Hγ"; first done.
-    iMod (inv_alloc N _ (lock_inv γ l R) with "[-HΦ]") as "#?".
-    { iIntros "!>". iExists false. by iFrame. }
-    iModIntro. iApply "HΦ". iExists l. eauto.
-  Qed.
-
-  Lemma try_acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} try_acquire lk
-    {{{ b, RET #b; if b is true then locked γ ∗ R else True }}}.
-  Proof.
-    iIntros (Φ) "#Hl HΦ". iDestruct "Hl" as (l ->) "#Hinv".
-    wp_rec. wp_bind (CmpXchg _ _ _). wp_swp. iInv N as "H". swp_step. iNext.
-    iDestruct "H" as ([]) "[Hl HR]".
-    - wp_cmpxchg_fail. iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
-      wp_pures. iApply ("HΦ" $! false). done.
-    - wp_cmpxchg_suc. iDestruct "HR" as "[Hγ HR]".
-      iModIntro. iSplitL "Hl"; first (iNext; iExists true; eauto).
-      rewrite /locked. wp_pures. by iApply ("HΦ" $! true with "[$Hγ $HR]").
-      Unshelve. exact 0%nat.
-  Qed.
-
-  Lemma acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
-  Proof.
-    iIntros (Φ) "#Hl HΦ". iLöb as "IH". wp_rec.
-    wp_apply (try_acquire_spec with "Hl"). iIntros ([]).
-    - iIntros "[Hlked HR]". wp_if. iApply "HΦ"; iFrame.
-    - iIntros "_". wp_if. iApply ("IH" with "[HΦ]"). auto.
-  Qed.
-
-  Lemma release_spec γ lk R :
-    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
-  Proof.
-    iIntros (Φ) "(Hlock & Hlocked & HR) HΦ".
-    iDestruct "Hlock" as (l ->) "#Hinv".
-    rewrite /release /=. wp_lam. wp_swp. iInv N as "H". swp_step. iNext.
-    iDestruct "H" as (b) "[Hl _]".
-    wp_store. iSplitR "HΦ"; last by iApply "HΦ".
-    iModIntro. iNext. iExists false. by iFrame.
-    Unshelve. exact 0%nat.
-  Qed.
-End proof.
-
-Typeclasses Opaque is_lock locked.
-
-Canonical Structure spin_lock {SI} {Σ: gFunctors SI} `{!heapG Σ, !lockG Σ} : lock Σ :=
-  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
-     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.

theories/examples/safety/ticket_lock.v

-From iris.program_logic Require Export weakestpre.
-From iris.heap_lang Require Export lang.
-From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation.
-From iris.algebra Require Import excl auth gset.
-From iris.examples.safety Require Export lock.
-Set Default Proof Using "Type".
-Import uPred.
-
-Definition wait_loop: val :=
-  rec: "wait_loop" "x" "lk" :=
-    let: "o" := !(Fst "lk") in
-    if: "x" = "o"
-      then #() (* my turn *)
-      else "wait_loop" "x" "lk".
-
-Definition newlock : val :=
-  λ: <>, ((* owner *) ref #0, (* next *) ref #0).
-
-Definition acquire : val :=
-  rec: "acquire" "lk" :=
-    let: "n" := !(Snd "lk") in
-    if: CAS (Snd "lk") "n" ("n" + #1)
-      then wait_loop "n" "lk"
-      else "acquire" "lk".
-
-Definition release : val :=
-  λ: "lk", (Fst "lk") <- !(Fst "lk") + #1.
-
-(** The CMRAs we need. *)
-Class tlockG {SI} (Σ: gFunctors SI) :=
-  tlock_G :> inG Σ (authR (prodUR (optionUR (exclR (natO SI))) (gset_disjUR nat))).
-Definition tlockΣ {SI} : gFunctors SI :=
-  #[ GFunctor (authR (prodUR (optionUR (exclR (natO SI))) (gset_disjUR nat))) ].
-
-Instance subG_tlockΣ {SI} {Σ: gFunctors SI} : subG tlockΣ Σ → tlockG Σ.
-Proof. solve_inG. Qed.
-
-Section proof.
-  Context {SI} {Σ: gFunctors SI} `{!heapG Σ, !tlockG Σ} (N : namespace).
-
-  Definition lock_inv (γ : gname) (lo ln : loc) (R : iProp Σ) : iProp Σ :=
-    (∃ o n : nat,
-      lo ↦ #o ∗ ln ↦ #n ∗
-      own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
-      ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))))%I.
-
-  Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
-    (∃ lo ln : loc,
-       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R))%I.
-
-  Definition issued (γ : gname) (x : nat) : iProp Σ :=
-    own γ (◯ (ε, GSet {[ x ]}))%I.
-
-  Definition locked (γ : gname) : iProp Σ := (∃ o, own γ (◯ (Excl' o, GSet ∅)))%I.
-
-  Global Instance lock_inv_ne γ lo ln :
-    NonExpansive (lock_inv γ lo ln).
-  Proof. solve_proper. Qed.
-  Global Instance is_lock_ne γ lk : NonExpansive (is_lock γ lk).
-  Proof. solve_proper. Qed.
-  Global Instance is_lock_persistent γ lk R : Persistent (is_lock γ lk R).
-  Proof. apply _. Qed.
-  Global Instance locked_timeless γ : Timeless (locked γ).
-  Proof. apply _. Qed.
-
-  Lemma locked_exclusive (γ : gname) : locked γ -∗ locked γ -∗ False.
-  Proof.
-    iDestruct 1 as (o1) "H1". iDestruct 1 as (o2) "H2".
-    iDestruct (own_valid_2 with "H1 H2") as %[[] _].
-  Qed.
-
-  Lemma newlock_spec (R : iProp Σ) :
-    {{{ R }}} newlock #() {{{ lk γ, RET lk; is_lock γ lk R }}}.
-  Proof.
-    iIntros (Φ) "HR HΦ". rewrite -wp_fupd. wp_lam.
-    wp_alloc ln as "Hln". wp_alloc lo as "Hlo".
-    iMod (own_alloc (● (Excl' 0%nat, GSet ∅) ⋅ ◯ (Excl' 0%nat, GSet ∅))) as (γ) "[Hγ Hγ']".
-    { by apply auth_both_valid. }
-    iMod (inv_alloc _ _ (lock_inv γ lo ln R) with "[-HΦ]").
-    { iNext. rewrite /lock_inv.
-      iExists 0%nat, 0%nat. iFrame. iLeft. by iFrame. }
-    wp_pures. iModIntro. iApply ("HΦ" $! (#lo, #ln)%V γ). iExists lo, ln. eauto.
-  Qed.
-
-  Lemma wait_loop_spec γ lk x R :
-    {{{ is_lock γ lk R ∗ issued γ x }}} wait_loop #x lk {{{ RET #(); locked γ ∗ R }}}.
-  Proof.
-    iIntros (Φ) "[Hl Ht] HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
-    iLöb as "IH". wp_rec. subst. wp_pures. wp_bind (! _)%E.
-    wp_swp 1%nat. iInv N as "Hlock". swp_step. iNext. iDestruct "Hlock" as (o n) "(Hlo & Hln & Ha)".
-    wp_load. destruct (decide (x = o)) as [->|Hneq].
-    - iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
-      + iModIntro. iSplitL "Hlo Hln Hainv Ht".
-        { iNext. iExists o, n. iFrame. }
-        wp_pures. case_bool_decide; [|done]. wp_if.
-        iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. simpl. eauto.
-      + iDestruct (own_valid_2 with "Ht Haown") as % [_ ?%gset_disj_valid_op].
-        set_solver.
-    - iModIntro. iSplitL "Hlo Hln Ha".
-      { iNext. iExists o, n. by iFrame. }
-      wp_pures. case_bool_decide; [simplify_eq |].
-      wp_if. iApply ("IH" with "Ht"). iNext. by iExact "HΦ".
-  Qed.
-
-  Lemma acquire_spec γ lk R :
-    {{{ is_lock γ lk R }}} acquire lk {{{ RET #(); locked γ ∗ R }}}.
-  Proof.
-    iIntros (ϕ) "Hl HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
-    iLöb as "IH". wp_rec. wp_bind (! _)%E. simplify_eq/=. wp_proj.
-    wp_swp 1%nat. iInv N as "Hlock". swp_step. iNext. iDestruct "Hlock" as (o n) "(Hlo & Hln & Ha)".
-    wp_load. iModIntro. iSplitL "Hlo Hln Ha".
-    { iNext. iExists o, n. by iFrame. }
-    wp_pures. wp_bind (CmpXchg _ _ _).
-    wp_swp 1%nat. iInv N as "Hlock". swp_step. iNext. iDestruct "Hlock" as (o' n') "(Hlo' & Hln' & Hauth & Haown)".
-    destruct (decide (#n' = #n))%V as [[= ->%Nat2Z.inj] | Hneq].
-    - iMod (own_update with "Hauth") as "[Hauth Hofull]".
-      { eapply auth_update_alloc, prod_local_update_2.
-        eapply (gset_disj_alloc_empty_local_update _ {[ n ]}).
-        apply (set_seq_S_end_disjoint 0). }
-      rewrite -(set_seq_S_end_union_L 0).
-      wp_cmpxchg_suc. iModIntro. iSplitL "Hlo' Hln' Haown Hauth".
-      { iNext. iExists o', (S n).
-        rewrite Nat2Z.inj_succ -Z.add_1_r. by iFrame. }
-      wp_pures.
-      iApply (wait_loop_spec γ (#lo, #ln) with "[-HΦ]").
-      + iFrame. rewrite /is_lock; eauto 10.
-      + by iNext.
-    - wp_cmpxchg_fail. iModIntro.
-      iSplitL "Hlo' Hln' Hauth Haown".
-      { iNext. iExists o', n'. by iFrame. }
-      wp_pures. by iApply "IH"; auto.
-  Qed.
-
-  Lemma release_spec γ lk R :
-    {{{ is_lock γ lk R ∗ locked γ ∗ R }}} release lk {{{ RET #(); True }}}.
-  Proof.
-    iIntros (Φ) "(Hl & Hγ & HR) HΦ". iDestruct "Hl" as (lo ln ->) "#Hinv".
-    iDestruct "Hγ" as (o) "Hγo".
-    wp_lam. wp_proj. wp_bind (! _)%E.
-    wp_swp 1%nat. iInv N as "Hlock". swp_step. iNext. iDestruct "Hlock" as (o' n) "(Hlo & Hln & Hauth & Haown)".
-    wp_load.
-    iDestruct (own_valid_2 with "Hauth Hγo") as
-      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
-    iModIntro. iSplitL "Hlo Hln Hauth Haown".
-    { iNext. iExists o, n. by iFrame. }
-    wp_pures.
-    wp_swp 1%nat. iInv N as "Hlock". swp_step. iNext. iDestruct "Hlock" as (o' n') "(Hlo & Hln & Hauth & Haown)".
-    iApply swp_fupd. wp_store.
-    iDestruct (own_valid_2 with "Hauth Hγo") as
-      %[[<-%Excl_included%leibniz_equiv _]%prod_included _]%auth_both_valid.
-    iDestruct "Haown" as "[[Hγo' _]|Haown]".
-    { iDestruct (own_valid_2 with "Hγo Hγo'") as %[[] ?]. }
-    iMod (own_update_2 with "Hauth Hγo") as "[Hauth Hγo]".
-    { apply auth_update, prod_local_update_1.
-      by apply option_local_update, (exclusive_local_update _ (Excl (S o))). }
-    iModIntro. iSplitR "HΦ"; last by iApply "HΦ".
-    iIntros "!> !>". iExists (S o), n'.
-    rewrite Nat2Z.inj_succ -Z.add_1_r. iFrame. iLeft. by iFrame.
-  Qed.
-End proof.
-
-Typeclasses Opaque is_lock issued locked.
-
-Canonical Structure ticket_lock {SI} {Σ: gFunctors SI} `{!heapG Σ, !tlockG Σ} : lock Σ :=
-  {| lock.locked_exclusive := locked_exclusive; lock.newlock_spec := newlock_spec;
-     lock.acquire_spec := acquire_spec; lock.release_spec := release_spec |}.