sts.v 6.95 KB
 Ralf Jung committed Feb 15, 2016 1 2 3 4 ``````From algebra Require Export sts. From program_logic Require Export invariants ghost_ownership. Import uPred. `````` Robbert Krebbers committed Feb 17, 2016 5 6 ``````Class stsG Λ Σ (sts : stsT) := StsG { sts_inG :> inG Λ Σ (stsRA sts); `````` Robbert Krebbers committed Feb 16, 2016 7 `````` sts_inhabited :> Inhabited (sts.state sts); `````` Ralf Jung committed Feb 15, 2016 8 ``````}. `````` Robbert Krebbers committed Feb 17, 2016 9 ``````Coercion sts_inG : stsG >-> inG. `````` Ralf Jung committed Feb 15, 2016 10 `````` `````` Ralf Jung committed Feb 22, 2016 11 12 13 14 15 16 ``````Definition stsF (sts : stsT) := constF (stsRA sts). Instance stsG_inGF sts `{Inhabited (sts.state sts)} `{inGF Λ Σ (stsF sts)} : stsG Λ Σ sts. Proof. split; try apply _. move:(@inGF_inG Λ Σ (stsF sts)). auto. Qed. `````` Ralf Jung committed Feb 15, 2016 17 ``````Section definitions. `````` Robbert Krebbers committed Feb 17, 2016 18 `````` Context `{i : stsG Λ Σ sts} (γ : gname). `````` Robbert Krebbers committed Feb 16, 2016 19 20 `````` Import sts. Definition sts_inv (φ : state sts → iPropG Λ Σ) : iPropG Λ Σ := `````` Robbert Krebbers committed Feb 17, 2016 21 `````` (∃ s, own γ (sts_auth s ∅) ★ φ s)%I. `````` Robbert Krebbers committed Feb 16, 2016 22 `````` Definition sts_ownS (S : states sts) (T : tokens sts) : iPropG Λ Σ:= `````` Robbert Krebbers committed Feb 17, 2016 23 `````` own γ (sts_frag S T). `````` Robbert Krebbers committed Feb 16, 2016 24 `````` Definition sts_own (s : state sts) (T : tokens sts) : iPropG Λ Σ := `````` Robbert Krebbers committed Feb 17, 2016 25 `````` own γ (sts_frag_up s T). `````` Robbert Krebbers committed Feb 16, 2016 26 27 `````` Definition sts_ctx (N : namespace) (φ: state sts → iPropG Λ Σ) : iPropG Λ Σ := inv N (sts_inv φ). `````` Ralf Jung committed Feb 15, 2016 28 ``````End definitions. `````` Robbert Krebbers committed Feb 17, 2016 29 30 31 32 ``````Instance: Params (@sts_inv) 5. Instance: Params (@sts_ownS) 5. Instance: Params (@sts_own) 6. Instance: Params (@sts_ctx) 6. `````` Ralf Jung committed Feb 15, 2016 33 34 `````` Section sts. `````` Robbert Krebbers committed Feb 17, 2016 35 `````` Context `{stsG Λ Σ sts} (φ : sts.state sts → iPropG Λ Σ). `````` Ralf Jung committed Feb 15, 2016 36 37 38 `````` Implicit Types N : namespace. Implicit Types P Q R : iPropG Λ Σ. Implicit Types γ : gname. `````` Robbert Krebbers committed Feb 16, 2016 39 40 41 42 43 `````` Implicit Types S : sts.states sts. Implicit Types T : sts.tokens sts. (** Setoids *) Global Instance sts_inv_ne n γ : `````` Robbert Krebbers committed Feb 17, 2016 44 `````` Proper (pointwise_relation _ (dist n) ==> dist n) (sts_inv γ). `````` Robbert Krebbers committed Feb 16, 2016 45 46 `````` Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed. Global Instance sts_inv_proper γ : `````` Robbert Krebbers committed Feb 17, 2016 47 `````` Proper (pointwise_relation _ (≡) ==> (≡)) (sts_inv γ). `````` Robbert Krebbers committed Feb 16, 2016 48 `````` Proof. by intros φ1 φ2 Hφ; rewrite /sts_inv; setoid_rewrite Hφ. Qed. `````` Robbert Krebbers committed Feb 17, 2016 49 `````` Global Instance sts_ownS_proper γ : Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS γ). `````` Robbert Krebbers committed Feb 16, 2016 50 `````` Proof. intros S1 S2 HS T1 T2 HT. by rewrite /sts_ownS HS HT. Qed. `````` Robbert Krebbers committed Feb 18, 2016 51 52 `````` Global Instance sts_own_proper γ s : Proper ((≡) ==> (≡)) (sts_own γ s). Proof. intros T1 T2 HT. by rewrite /sts_own HT. Qed. `````` Robbert Krebbers committed Feb 16, 2016 53 `````` Global Instance sts_ctx_ne n γ N : `````` Robbert Krebbers committed Feb 17, 2016 54 `````` Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N). `````` Robbert Krebbers committed Feb 16, 2016 55 56 `````` Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed. Global Instance sts_ctx_proper γ N : `````` Robbert Krebbers committed Feb 17, 2016 57 `````` Proper (pointwise_relation _ (≡) ==> (≡)) (sts_ctx γ N). `````` Robbert Krebbers committed Feb 16, 2016 58 `````` Proof. by intros φ1 φ2 Hφ; rewrite /sts_ctx Hφ. Qed. `````` Ralf Jung committed Feb 15, 2016 59 `````` `````` Ralf Jung committed Feb 15, 2016 60 61 `````` (* The same rule as implication does *not* hold, as could be shown using sts_frag_included. *) `````` Ralf Jung committed Feb 17, 2016 62 `````` Lemma sts_ownS_weaken E γ S1 S2 T1 T2 : `````` 63 `````` T2 ⊆ T1 → S1 ⊆ S2 → sts.closed S2 T2 → `````` Robbert Krebbers committed Feb 19, 2016 64 `````` sts_ownS γ S1 T1 ⊑ (|={E}=> sts_ownS γ S2 T2). `````` 65 `````` Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed. `````` Ralf Jung committed Feb 15, 2016 66 `````` `````` Ralf Jung committed Feb 17, 2016 67 `````` Lemma sts_own_weaken E γ s S T1 T2 : `````` 68 `````` T2 ⊆ T1 → s ∈ S → sts.closed S T2 → `````` Robbert Krebbers committed Feb 19, 2016 69 `````` sts_own γ s T1 ⊑ (|={E}=> sts_ownS γ S T2). `````` 70 `````` Proof. intros ???. by apply own_update, sts_update_frag_up. Qed. `````` Ralf Jung committed Feb 15, 2016 71 `````` `````` Ralf Jung committed Feb 17, 2016 72 `````` Lemma sts_ownS_op γ S1 S2 T1 T2 : `````` Ralf Jung committed Feb 17, 2016 73 `````` T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 → `````` Ralf Jung committed Feb 17, 2016 74 `````` sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I. `````` Robbert Krebbers committed Feb 17, 2016 75 `````` Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed. `````` Ralf Jung committed Feb 17, 2016 76 `````` `````` Ralf Jung committed Feb 17, 2016 77 78 `````` Lemma sts_alloc E N s : nclose N ⊆ E → `````` Robbert Krebbers committed Feb 19, 2016 79 `````` ▷ φ s ⊑ (|={E}=> ∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)). `````` Ralf Jung committed Feb 15, 2016 80 `````` Proof. `````` Ralf Jung committed Feb 17, 2016 81 `````` intros HN. eapply sep_elim_True_r. `````` Robbert Krebbers committed Feb 17, 2016 82 `````` { apply (own_alloc (sts_auth s (⊤ ∖ sts.tok s)) N). `````` Robbert Krebbers committed Feb 17, 2016 83 `````` apply sts_auth_valid; set_solver. } `````` Ralf Jung committed Feb 17, 2016 84 85 `````` rewrite pvs_frame_l. rewrite -(pvs_mask_weaken N E) //. apply pvs_strip_pvs. `````` Ralf Jung committed Feb 15, 2016 86 `````` rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ). `````` Ralf Jung committed Feb 20, 2016 87 `````` trans (▷ sts_inv γ φ ★ sts_own γ s (⊤ ∖ sts.tok s))%I. `````` Ralf Jung committed Feb 17, 2016 88 89 `````` { rewrite /sts_inv -(exist_intro s) later_sep. rewrite [(_ ★ ▷ φ _)%I]comm -assoc. apply sep_mono_r. `````` Robbert Krebbers committed Feb 17, 2016 90 `````` by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. } `````` Robbert Krebbers committed Feb 16, 2016 91 `````` rewrite (inv_alloc N) /sts_ctx pvs_frame_r. `````` Ralf Jung committed Feb 15, 2016 92 93 94 `````` by rewrite always_and_sep_l. Qed. `````` Robbert Krebbers committed Feb 16, 2016 95 `````` Lemma sts_opened E γ S T : `````` Robbert Krebbers committed Feb 17, 2016 96 `````` (▷ sts_inv γ φ ★ sts_ownS γ S T) `````` Robbert Krebbers committed Feb 19, 2016 97 `````` ⊑ (|={E}=> ∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)). `````` Ralf Jung committed Feb 15, 2016 98 `````` Proof. `````` Robbert Krebbers committed Feb 16, 2016 99 `````` rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s. `````` Ralf Jung committed Feb 15, 2016 100 101 102 103 `````` rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono. rewrite -(exist_intro s). rewrite [(_ ★ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ ★ _)%I]comm. rewrite own_valid_l discrete_validI. `````` Robbert Krebbers committed Feb 16, 2016 104 105 106 `````` rewrite -!assoc. apply const_elim_sep_l=> Hvalid. assert (s ∈ S) by (by eapply sts_auth_frag_valid_inv, discrete_valid). rewrite const_equiv // left_id comm sts_op_auth_frag //. `````` 107 108 109 `````` assert (✓ sts_frag S T) as Hv by by eapply cmra_valid_op_r, discrete_valid. apply (Hv 0). `````` Ralf Jung committed Feb 15, 2016 110 111 `````` Qed. `````` Robbert Krebbers committed Feb 16, 2016 112 `````` Lemma sts_closing E γ s T s' T' : `````` Ralf Jung committed Feb 20, 2016 113 `````` sts.steps (s, T) (s', T') → `````` Robbert Krebbers committed Feb 19, 2016 114 `````` (▷ φ s' ★ own γ (sts_auth s T)) ⊑ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T'). `````` Ralf Jung committed Feb 15, 2016 115 `````` Proof. `````` Robbert Krebbers committed Feb 16, 2016 116 `````` intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s'). `````` Ralf Jung committed Feb 15, 2016 117 `````` rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc. `````` Robbert Krebbers committed Feb 16, 2016 118 `````` rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro. `````` Ralf Jung committed Feb 15, 2016 119 `````` rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval. `````` Ralf Jung committed Feb 20, 2016 120 `````` trans (|={E}=> own γ (sts_auth s' T'))%I. `````` Robbert Krebbers committed Feb 16, 2016 121 `````` { by apply own_update, sts_update_auth. } `````` Ralf Jung committed Feb 20, 2016 122 `````` by rewrite -own_op sts_op_auth_frag_up. `````` Ralf Jung committed Feb 15, 2016 123 `````` Qed. `````` Ralf Jung committed Feb 15, 2016 124 `````` `````` Ralf Jung committed Feb 15, 2016 125 126 `````` Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}. `````` Robbert Krebbers committed Feb 18, 2016 127 `````` Lemma sts_fsaS E N P (Ψ : V → iPropG Λ Σ) γ S T : `````` Ralf Jung committed Feb 15, 2016 128 `````` fsaV → nclose N ⊆ E → `````` Robbert Krebbers committed Feb 17, 2016 129 130 `````` P ⊑ sts_ctx γ N φ → P ⊑ (sts_ownS γ S T ★ ∀ s, `````` Ralf Jung committed Feb 15, 2016 131 `````` ■ (s ∈ S) ★ ▷ φ s -★ `````` Ralf Jung committed Feb 15, 2016 132 `````` fsa (E ∖ nclose N) (λ x, ∃ s' T', `````` Ralf Jung committed Feb 20, 2016 133 `````` ■ sts.steps (s, T) (s', T') ★ ▷ φ s' ★ `````` Robbert Krebbers committed Feb 18, 2016 134 135 `````` (sts_own γ s' T' -★ Ψ x))) → P ⊑ fsa E Ψ. `````` Ralf Jung committed Feb 15, 2016 136 `````` Proof. `````` Robbert Krebbers committed Feb 16, 2016 137 `````` rewrite /sts_ctx=>? HN Hinv Hinner. `````` Ralf Jung committed Feb 15, 2016 138 139 `````` eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}. apply wand_intro_l. rewrite assoc. `````` Robbert Krebbers committed Feb 16, 2016 140 `````` rewrite (sts_opened (E ∖ N)) !pvs_frame_r !sep_exist_r. `````` Ralf Jung committed Feb 15, 2016 141 142 `````` apply (fsa_strip_pvs fsa). apply exist_elim=>s. rewrite (forall_elim s). rewrite [(▷_ ★ _)%I]comm. `````` Ralf Jung committed Feb 20, 2016 143 144 145 `````` eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first. { rewrite assoc [(_ ★ own _ _)%I]comm -assoc. done. } rewrite fsa_frame_l. `````` Ralf Jung committed Feb 15, 2016 146 `````` apply (fsa_mono_pvs fsa)=> x. `````` Ralf Jung committed Feb 15, 2016 147 `````` rewrite sep_exist_l; apply exist_elim=> s'. `````` Ralf Jung committed Feb 15, 2016 148 149 `````` rewrite sep_exist_l; apply exist_elim=>T'. rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep. `````` Ralf Jung committed Feb 15, 2016 150 `````` rewrite assoc [(_ ★ (_ -★ _))%I]comm -assoc. `````` Robbert Krebbers committed Feb 16, 2016 151 `````` rewrite (sts_closing (E ∖ N)) //; []. `````` Ralf Jung committed Feb 15, 2016 152 153 154 155 `````` rewrite pvs_frame_l. apply pvs_mono. by rewrite assoc [(_ ★ ▷_)%I]comm -assoc wand_elim_l. Qed. `````` Robbert Krebbers committed Feb 18, 2016 156 `````` Lemma sts_fsa E N P (Ψ : V → iPropG Λ Σ) γ s0 T : `````` Ralf Jung committed Feb 15, 2016 157 `````` fsaV → nclose N ⊆ E → `````` Robbert Krebbers committed Feb 17, 2016 158 159 `````` P ⊑ sts_ctx γ N φ → P ⊑ (sts_own γ s0 T ★ ∀ s, `````` Robbert Krebbers committed Feb 16, 2016 160 `````` ■ (s ∈ sts.up s0 T) ★ ▷ φ s -★ `````` Ralf Jung committed Feb 15, 2016 161 `````` fsa (E ∖ nclose N) (λ x, ∃ s' T', `````` Ralf Jung committed Feb 20, 2016 162 `````` ■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★ `````` Robbert Krebbers committed Feb 18, 2016 163 164 `````` (sts_own γ s' T' -★ Ψ x))) → P ⊑ fsa E Ψ. `````` Robbert Krebbers committed Feb 16, 2016 165 `````` Proof. apply sts_fsaS. Qed. `````` Ralf Jung committed Feb 15, 2016 166 ``End sts.``