From fcca059352aa86de7f5e13cc5d5285b32fae9e7a Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 15 Feb 2016 14:34:33 +0100 Subject: [PATCH] prove sts_alloc; play around with modules and namespaces for sts --- algebra/cmra.v | 4 ++- algebra/upred.v | 8 ++--- program_logic/ownership.v | 2 +- program_logic/sts.v | 68 ++++++++++++++++++++++++++++++--------- 4 files changed, 60 insertions(+), 22 deletions(-) diff --git a/algebra/cmra.v b/algebra/cmra.v index b3f8f94..f8eff51 100644 --- a/algebra/cmra.v +++ b/algebra/cmra.v @@ -466,7 +466,7 @@ Class RA A `{Equiv A, Unit A, Op A, Valid A, Minus A} := { Section discrete. Context {A : cofeT} `{∀ x : A, Timeless x}. - Context `{Unit A, Op A, Valid A, Minus A} (ra : RA A). + Context {v : Valid A} `{Unit A, Op A, Minus A} (ra : RA A). Instance discrete_validN : ValidN A := λ n x, ✓ x. Definition discrete_cmra_mixin : CMRAMixin A. @@ -487,6 +487,8 @@ Section discrete. Lemma discrete_update (x y : discreteRA) : (∀ z, ✓ (x ⋅ z) → ✓ (y ⋅ z)) → x ~~> y. Proof. intros Hvalid z n; apply Hvalid. Qed. + Lemma discrete_valid (x : discreteRA) : v x → validN_valid x. + Proof. move=>Hx n. exact Hx. Qed. End discrete. (** ** CMRA for the unit type *) diff --git a/algebra/upred.v b/algebra/upred.v index 0befa18..32f09fd 100644 --- a/algebra/upred.v +++ b/algebra/upred.v @@ -320,13 +320,13 @@ Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M). Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_validN. Qed. Global Instance always_proper : Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _. -Global Instance own_ne n : Proper (dist n ==> dist n) (@uPred_ownM M). +Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M). Proof. by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first [rewrite -(dist_le _ _ _ _ Ha); last lia |rewrite (dist_le _ _ _ _ Ha); last lia]. Qed. -Global Instance own_proper : Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _. +Global Instance ownM_proper : Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _. Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M). Proof. unfold uPred_iff; solve_proper. Qed. Global Instance iff_proper : @@ -899,7 +899,7 @@ Qed. Global Instance eq_timeless {A : cofeT} (a b : A) : Timeless a → TimelessP (a ≡ b : uPred M)%I. Proof. by intro; apply timelessP_spec=> x n ??; apply equiv_dist, timeless. Qed. -Global Instance own_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a). +Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a). Proof. intros ?; apply timelessP_spec=> x [|n] ?? //; apply cmra_included_includedN, cmra_timeless_included_l; eauto using cmra_validN_le. @@ -929,7 +929,7 @@ Global Instance valid_always_stable {A : cmraT} (a : A) : AS (✓ a : uPred M)%I Proof. by intros; rewrite /AlwaysStable always_valid. Qed. Global Instance later_always_stable P : AS P → AS (▷ P). Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed. -Global Instance own_unit_always_stable (a : M) : AS (uPred_ownM (unit a)). +Global Instance ownM_unit_always_stable (a : M) : AS (uPred_ownM (unit a)). Proof. by rewrite /AlwaysStable always_ownM_unit. Qed. Global Instance default_always_stable {A} P (Q : A → uPred M) (mx : option A) : AS P → (∀ x, AS (Q x)) → AS (default P mx Q). diff --git a/program_logic/ownership.v b/program_logic/ownership.v index 9ee1d0e..913b0db 100644 --- a/program_logic/ownership.v +++ b/program_logic/ownership.v @@ -22,7 +22,7 @@ Implicit Types m : iGst Λ Σ. Global Instance ownI_contractive i : Contractive (@ownI Λ Σ i). Proof. intros n P Q HPQ. rewrite /ownI. - apply uPred.own_ne, Res_ne; auto; apply singleton_ne, to_agree_ne. + apply uPred.ownM_ne, Res_ne; auto; apply singleton_ne, to_agree_ne. by apply Next_contractive=> j ?; rewrite (HPQ j). Qed. Lemma always_ownI i P : (□ ownI i P)%I ≡ ownI i P. diff --git a/program_logic/sts.v b/program_logic/sts.v index b25ed4d..bf864e2 100644 --- a/program_logic/sts.v +++ b/program_logic/sts.v @@ -1,32 +1,68 @@ From algebra Require Export sts. +From algebra Require Import dra. From program_logic Require Export invariants ghost_ownership. Import uPred. -Class StsInG Λ Σ (i : gid) {A B} (R : relation A) (tok : A → set B) := { - sts_inG :> InG Λ Σ i (stsRA R tok); +Local Arguments valid _ _ !_ /. +Local Arguments op _ _ !_ !_ /. +Local Arguments unit _ _ !_ /. + +Module sts. +Record Sts {A B} := { + st : relation A; + tok : A → set B; +}. +Arguments Sts : clear implicits. + +Class InG Λ Σ (i : gid) {A B} (sts : Sts A B) := { + inG :> ghost_ownership.InG Λ Σ i (stsRA sts.(st) sts.(tok)); }. Section definitions. - Context {Λ Σ A B} (i : gid) (R : relation A) (tok : A → set B) - `{!StsInG Λ Σ i R tok} (γ : gname). - Definition sts_inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ := - (∃ s, own i γ (sts_auth R tok s set_all) ★ φ s)%I. - Definition sts_states (S : set A) (T: set B) : iPropG Λ Σ := - (■ sts.closed R tok S T ∧ own i γ (sts_frag R tok S T))%I. - Definition sts_state (s : A) (T: set B) : iPropG Λ Σ := - own i γ (sts_frag R tok (sts.up R tok s T) T). - Definition sts_ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := - inv N (sts_inv φ). + Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ i sts} (γ : gname). + Definition inv (φ : A → iPropG Λ Σ) : iPropG Λ Σ := + (∃ s, own i γ (sts_auth sts.(st) sts.(tok) s set_empty) ★ φ s)%I. + Definition states (S : set A) (T: set B) : iPropG Λ Σ := + (■ sts.closed sts.(st) sts.(tok) S T ∧ + own i γ (sts_frag sts.(st) sts.(tok) S T))%I. + Definition state (s : A) (T: set B) : iPropG Λ Σ := + own i γ (sts_frag sts.(st) sts.(tok) (sts.up sts.(st) sts.(tok) s T) T). + Definition ctx (N : namespace) (φ : A → iPropG Λ Σ) : iPropG Λ Σ := + invariants.inv N (inv φ). End definitions. -Instance: Params (@sts_inv) 9. -Instance: Params (@sts_states) 9. -Instance: Params (@sts_ctx) 10. +Instance: Params (@inv) 8. +Instance: Params (@states) 8. +Instance: Params (@ctx) 9. Section sts. - Context `{StsInG Λ Σ StsI (A:=A) R tok}. + Context {Λ Σ A B} (i : gid) (sts : Sts A B) `{!InG Λ Σ StsI sts}. Context (φ : A → iPropG Λ Σ). Implicit Types N : namespace. Implicit Types P Q R : iPropG Λ Σ. Implicit Types γ : gname. + Lemma alloc N s : + φ s ⊑ pvs N N (∃ γ, ctx StsI sts γ N φ ∧ state StsI sts γ s (set_all ∖ sts.(tok) s)). + Proof. + eapply sep_elim_True_r. + { eapply (own_alloc StsI (sts_auth sts.(st) sts.(tok) s (set_all ∖ sts.(tok) s)) N). + apply discrete_valid=>/=. solve_elem_of. } + rewrite pvs_frame_l. apply pvs_strip_pvs. + rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ). + transitivity (▷ inv StsI sts γ φ ★ state StsI sts γ s (set_all ∖ sts.(tok) s))%I. + { rewrite /inv -later_intro -(exist_intro s). + rewrite [(_ ★ φ _)%I]comm -assoc. apply sep_mono; first done. + rewrite -own_op. apply equiv_spec, own_proper. + split; first split; simpl. + - intros; solve_elem_of-. + - intros _. split_ands; first by solve_elem_of-. + + apply sts.closed_up. solve_elem_of-. + + constructor; last solve_elem_of-. apply sts.elem_of_up. + - intros _. constructor. solve_elem_of-. } + rewrite (inv_alloc N) /ctx pvs_frame_r. apply pvs_mono. + by rewrite always_and_sep_l. + Qed. + +End sts. + End sts. -- GitLab