From 98e519742bdea653d586a4b696aa0c26b2a6bc84 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 9 Aug 2016 15:31:59 +0200 Subject: [PATCH] STS: accessor for sts_inv --- algebra/sts.v | 6 ++++-- program_logic/sts.v | 44 ++++++++++++++++++++++++++++++++++---------- 2 files changed, 38 insertions(+), 12 deletions(-) diff --git a/algebra/sts.v b/algebra/sts.v index ee8570cc..c57aec29 100644 --- a/algebra/sts.v +++ b/algebra/sts.v @@ -32,6 +32,7 @@ Notation steps := (rtc step). Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop := | Frame_step T1 T2 : T1 ⊥ tok s1 ∪ T → step (s1,T1) (s2,T2) → frame_step T s1 s2. +Notation frame_steps T := (rtc (frame_step T)). (** ** Closure under frame steps *) Record closed (S : states sts) (T : tokens sts) : Prop := Closed { @@ -39,7 +40,7 @@ Record closed (S : states sts) (T : tokens sts) : Prop := Closed { closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S }. Definition up (s : state sts) (T : tokens sts) : states sts := - {[ s' | rtc (frame_step T) s s' ]}. + {[ s' | frame_steps T s s' ]}. Definition up_set (S : states sts) (T : tokens sts) : states sts := S ≫= λ s, up s T. @@ -86,7 +87,7 @@ Qed. (** ** Properties of closure under frame steps *) Lemma closed_steps S T s1 s2 : - closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S. + closed S T → s1 ∈ S → frame_steps T s1 s2 → s2 ∈ S. Proof. induction 3; eauto using closed_step. Qed. Lemma closed_op T1 T2 S1 S2 : closed S1 T1 → closed S2 T2 → closed (S1 ∩ S2) (T1 ∪ T2). @@ -160,6 +161,7 @@ Proof. move=> ?? s [s' [? ?]]. eauto using closed_steps. Qed. End sts. Notation steps := (rtc step). +Notation frame_steps T := (rtc (frame_step T)). (* The type of bounds we can give to the state of an STS. This is the type that we equip with an RA structure. *) diff --git a/program_logic/sts.v b/program_logic/sts.v index 60f34f16..6e440de8 100644 --- a/program_logic/sts.v +++ b/program_logic/sts.v @@ -46,7 +46,7 @@ Section definitions. Proof. apply _. Qed. End definitions. -Typeclasses Opaque sts_own sts_ownS sts_ctx. +Typeclasses Opaque sts_own sts_ownS sts_inv sts_ctx. Instance: Params (@sts_inv) 5. Instance: Params (@sts_ownS) 5. Instance: Params (@sts_own) 6. @@ -85,17 +85,16 @@ Section sts. { apply sts_auth_valid; set_solver. } iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ \$]". iVs (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto. - iNext. iExists s. by iFrame. + rewrite /sts_inv. iNext. iExists s. by iFrame. Qed. - Lemma sts_openS E N γ S T : - nclose N ⊆ E → - sts_ctx γ N φ ★ sts_ownS γ S T ={E,E∖N}=> ∃ s, + Lemma sts_accS E γ S T : + ▷ sts_inv γ φ ★ sts_ownS γ S T ={E}=> ∃ s, ■ (s ∈ S) ★ ▷ φ s ★ ∀ s' T', - ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'. + ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'. Proof. - iIntros (?) "[#? Hγf]". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own. - iInv N as (s) "[>Hγ Hφ]" "Hclose". + iIntros "[Hinv Hγf]". rewrite /sts_ownS /sts_inv /sts_own. + iDestruct "Hinv" as (s) "[>Hγ Hφ]". iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "#Hγ") as %Hvalid. assert (s ∈ S) by eauto using sts_auth_frag_valid_inv. assert (✓ sts_frag S T) as [??] by eauto using cmra_valid_op_r. @@ -104,13 +103,38 @@ Section sts. iIntros (s' T') "[% Hφ]". iVs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth. iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ \$]". - iApply "Hclose". iNext; iExists s'; by iFrame. + iVsIntro. iNext. iExists s'; by iFrame. + Qed. + + Lemma sts_acc E γ s0 T : + ▷ sts_inv γ φ ★ sts_own γ s0 T ={E}=> ∃ s, + ■ sts.frame_steps T s0 s ★ ▷ φ s ★ ∀ s' T', + ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E}=★ ▷ sts_inv γ φ ★ sts_own γ s' T'. + Proof. by apply sts_accS. Qed. + + Lemma sts_openS E N γ S T : + nclose N ⊆ E → + sts_ctx γ N φ ★ sts_ownS γ S T ={E,E∖N}=> ∃ s, + ■ (s ∈ S) ★ ▷ φ s ★ ∀ s' T', + ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'. + Proof. + iIntros (?) "[#? Hγf]". rewrite /sts_ctx. iInv N as "Hinv" "Hclose". + (* The following is essentially a very trivial composition of the accessors + [sts_acc] and [inv_open] -- but since we don't have any good support + for that currently, this gets more tedious than it should, with us having + to unpack and repack various proofs. + TODO: Make this mostly automatic, by supporting "opening accessors + around accessors". *) + iVs (sts_accS with "[Hinv Hγf]") as (s) "(?&?& HclSts)"; first by iFrame. + iVsIntro. iExists s. iFrame. iIntros (s' T') "H". + iVs ("HclSts" \$! s' T' with "H") as "(Hinv & ?)". iFrame. + iVs ("Hclose" with "Hinv"). done. Qed. Lemma sts_open E N γ s0 T : nclose N ⊆ E → sts_ctx γ N φ ★ sts_own γ s0 T ={E,E∖N}=> ∃ s, - ■ (s ∈ sts.up s0 T) ★ ▷ φ s ★ ∀ s' T', + ■ (sts.frame_steps T s0 s) ★ ▷ φ s ★ ∀ s' T', ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ={E∖N,E}=★ sts_own γ s' T'. Proof. by apply sts_openS. Qed. End sts. -- 2.26.2