specification.v 1.42 KB
 Robbert Krebbers committed Feb 24, 2016 1 2 3 4 5 6 ``````From program_logic Require Export hoare. From barrier Require Export barrier. From barrier Require Import proof. Import uPred. Section spec. `````` Ralf Jung committed Mar 07, 2016 7 ``````Context {Σ : gFunctors} `{!heapG Σ} `{!barrierG Σ}. `````` Robbert Krebbers committed Feb 24, 2016 8 9 10 11 12 13 `````` Local Notation iProp := (iPropG heap_lang Σ). (* TODO: Maybe notation for LocV (and Loc)? *) Lemma barrier_spec (heapN N : namespace) : heapN ⊥ N → `````` Robbert Krebbers committed Feb 27, 2016 14 `````` ∃ recv send : loc → iProp -n> iProp, `````` Robbert Krebbers committed Mar 02, 2016 15 16 `````` (∀ P, heap_ctx heapN ⊑ {{ True }} newbarrier #() {{ λ v, ∃ l : loc, v = LocV l ★ recv l P ★ send l P }}) ∧ `````` Robbert Krebbers committed Feb 24, 2016 17 18 `````` (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧ (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧ `````` Ralf Jung committed Mar 01, 2016 19 `````` (∀ l P Q, recv l (P ★ Q) ={N}=> recv l P ★ recv l Q) ∧ `````` Robbert Krebbers committed Feb 24, 2016 20 21 22 23 24 25 `````` (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)). Proof. intros HN. exists (λ l, CofeMor (recv heapN N l)), (λ l, CofeMor (send heapN N l)). split_and?; simpl. - intros P. apply: always_intro. apply impl_intro_r. `````` Ralf Jung committed Feb 28, 2016 26 `````` rewrite -(newbarrier_spec heapN N P) // always_and_sep_r. `````` Robbert Krebbers committed Feb 24, 2016 27 28 29 30 31 `````` apply sep_mono_r, forall_intro=>l; apply wand_intro_l. by rewrite right_id -(exist_intro l) const_equiv // left_id. - intros l P. apply ht_alt. by rewrite -signal_spec right_id. - intros l P. apply ht_alt. by rewrite -(wait_spec heapN N l P) wand_diag right_id. `````` Ralf Jung committed Mar 01, 2016 32 `````` - intros l P Q. apply vs_alt. rewrite -(recv_split heapN N N l P Q) //. `````` Ralf Jung committed Mar 01, 2016 33 `````` - intros l P Q. apply recv_weaken. `````` Robbert Krebbers committed Feb 24, 2016 34 35 ``````Qed. End spec.``````