Robbert Krebbers committed Feb 04, 2016 1 ``````Require Export program_logic.hoare. `````` Ralf Jung committed Feb 08, 2016 2 ``````Require Import program_logic.wsat program_logic.ownership. `````` Robbert Krebbers committed Jan 20, 2016 3 4 5 6 7 8 9 ``````Local Hint Extern 10 (_ ≤ _) => omega. Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of. Local Hint Extern 10 (✓{_} _) => repeat match goal with H : wsat _ _ _ _ |- _ => apply wsat_valid in H end; solve_validN. Section adequacy. `````` Robbert Krebbers committed Feb 01, 2016 10 11 12 13 ``````Context {Λ : language} {Σ : iFunctor}. Implicit Types e : expr Λ. Implicit Types Q : val Λ → iProp Λ Σ. Implicit Types m : iGst Λ Σ. `````` Robbert Krebbers committed Jan 20, 2016 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 ``````Transparent uPred_holds. Notation wptp n := (Forall3 (λ e Q r, uPred_holds (wp coPset_all e Q) n r)). Lemma wptp_le Qs es rs n n' : ✓{n'} (big_op rs) → wptp n es Qs rs → n' ≤ n → wptp n' es Qs rs. Proof. induction 2; constructor; eauto using uPred_weaken. Qed. Lemma nsteps_wptp Qs k n tσ1 tσ2 rs1 : nsteps step k tσ1 tσ2 → 1 < n → wptp (k + n) (tσ1.1) Qs rs1 → wsat (k + n) coPset_all (tσ1.2) (big_op rs1) → ∃ rs2 Qs', wptp n (tσ2.1) (Qs ++ Qs') rs2 ∧ wsat n coPset_all (tσ2.2) (big_op rs2). Proof. intros Hsteps Hn; revert Qs rs1. induction Hsteps as [|k ?? tσ3 [e1 σ1 e2 σ2 ef t1 t2 ?? Hstep] Hsteps IH]; simplify_equality'; intros Qs rs. { by intros; exists rs, []; rewrite right_id_L. } intros (Qs1&?&rs1&?&->&->&?& (Q&Qs2&r&rs2&->&->&Hwp&?)%Forall3_cons_inv_l)%Forall3_app_inv_l ?. destruct (wp_step_inv coPset_all ∅ Q e1 (k + n) (S (k + n)) σ1 r (big_op (rs1 ++ rs2))) as [_ Hwpstep]; eauto using values_stuck. { by rewrite right_id_L -big_op_cons Permutation_middle. } destruct (Hwpstep e2 σ2 ef) as (r2&r2'&Hwsat&?&?); auto; clear Hwpstep. revert Hwsat; rewrite big_op_app right_id_L=>Hwsat. destruct ef as [e'|]. * destruct (IH (Qs1 ++ Q :: Qs2 ++ [λ _, True%I]) (rs1 ++ r2 :: rs2 ++ [r2'])) as (rs'&Qs'&?&?). { apply Forall3_app, Forall3_cons, Forall3_app, Forall3_cons, Forall3_nil; eauto using wptp_le. } { by rewrite -Permutation_middle /= (associative (++)) (commutative (++)) /= associative big_op_app. } exists rs', ([λ _, True%I] ++ Qs'); split; auto. by rewrite (associative _ _ _ Qs') -(associative _ Qs1). * apply (IH (Qs1 ++ Q :: Qs2) (rs1 ++ r2 ⋅ r2' :: rs2)). { rewrite /option_list right_id_L. apply Forall3_app, Forall3_cons; eauto using wptp_le. `````` Robbert Krebbers committed Feb 01, 2016 50 `````` apply uPred_weaken with r2 (k + n); eauto using cmra_included_l. } `````` Robbert Krebbers committed Jan 20, 2016 51 52 53 54 55 56 57 `````` by rewrite -Permutation_middle /= big_op_app. Qed. Lemma ht_adequacy_steps P Q k n e1 t2 σ1 σ2 r1 : {{ P }} e1 @ coPset_all {{ Q }} → nsteps step k ([e1],σ1) (t2,σ2) → 1 < n → wsat (k + n) coPset_all σ1 r1 → P (k + n) r1 → `````` Robbert Krebbers committed Feb 10, 2016 58 `````` ∃ rs2 Qs', wptp n t2 (Q :: Qs') rs2 ∧ wsat n coPset_all σ2 (big_op rs2). `````` Robbert Krebbers committed Jan 20, 2016 59 ``````Proof. `````` Robbert Krebbers committed Feb 10, 2016 60 61 `````` intros Hht ????; apply (nsteps_wptp [Q] k n ([e1],σ1) (t2,σ2) [r1]); rewrite /big_op ?right_id; auto. `````` Robbert Krebbers committed Jan 20, 2016 62 `````` constructor; last constructor. `````` Robbert Krebbers committed Feb 01, 2016 63 `````` apply Hht with r1 (k + n); eauto using cmra_included_unit. `````` Robbert Krebbers committed Feb 10, 2016 64 `````` eapply uPred.const_intro; eauto. `````` Robbert Krebbers committed Jan 20, 2016 65 ``````Qed. `````` Ralf Jung committed Jan 25, 2016 66 67 68 69 ``````Lemma ht_adequacy_own Q e1 t2 σ1 m σ2 : ✓m → {{ ownP σ1 ★ ownG m }} e1 @ coPset_all {{ Q }} → rtc step ([e1],σ1) (t2,σ2) → `````` Robbert Krebbers committed Feb 10, 2016 70 `````` ∃ rs2 Qs', wptp 3 t2 (Q :: Qs') rs2 ∧ wsat 3 coPset_all σ2 (big_op rs2). `````` Ralf Jung committed Jan 25, 2016 71 ``````Proof. `````` Robbert Krebbers committed Feb 01, 2016 72 `````` intros Hv ? [k ?]%rtc_nsteps. `````` Robbert Krebbers committed Feb 04, 2016 73 `````` eapply ht_adequacy_steps with (r1 := (Res ∅ (Excl σ1) (Some m))); eauto; [|]. `````` Robbert Krebbers committed Feb 01, 2016 74 `````` { by rewrite Nat.add_comm; apply wsat_init, cmra_valid_validN. } `````` Robbert Krebbers committed Feb 04, 2016 75 `````` exists (Res ∅ (Excl σ1) ∅), (Res ∅ ∅ (Some m)); split_ands. `````` Robbert Krebbers committed Feb 01, 2016 76 77 78 `````` * by rewrite Res_op ?left_id ?right_id. * by rewrite /uPred_holds /=. * by apply ownG_spec. `````` Ralf Jung committed Jan 25, 2016 79 80 ``````Qed. Theorem ht_adequacy_result E φ e v t2 σ1 m σ2 : `````` Robbert Krebbers committed Feb 01, 2016 81 `````` ✓ m → `````` Ralf Jung committed Jan 25, 2016 82 `````` {{ ownP σ1 ★ ownG m }} e @ E {{ λ v', ■ φ v' }} → `````` Robbert Krebbers committed Jan 20, 2016 83 84 85 `````` rtc step ([e], σ1) (of_val v :: t2, σ2) → φ v. Proof. `````` Ralf Jung committed Jan 25, 2016 86 87 88 `````` intros Hv ? Hs. destruct (ht_adequacy_own (λ v', ■ φ v')%I e (of_val v :: t2) σ1 m σ2) as (rs2&Qs&Hwptp&?); auto. `````` Robbert Krebbers committed Jan 20, 2016 89 90 `````` { by rewrite -(ht_mask_weaken E coPset_all). } inversion Hwptp as [|?? r ?? rs Hwp _]; clear Hwptp; subst. `````` Ralf Jung committed Jan 25, 2016 91 `````` apply wp_value_inv in Hwp; destruct (Hwp (big_op rs) 3 ∅ σ2) as [r' []]; auto. `````` Robbert Krebbers committed Jan 20, 2016 92 93 `````` by rewrite right_id_L. Qed. `````` Ralf Jung committed Jan 25, 2016 94 ``````Lemma ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2 : `````` Robbert Krebbers committed Feb 01, 2016 95 `````` ✓ m → `````` Ralf Jung committed Jan 25, 2016 96 `````` {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} → `````` Robbert Krebbers committed Jan 20, 2016 97 98 99 `````` rtc step ([e1], σ1) (t2, σ2) → e2 ∈ t2 → to_val e2 = None → reducible e2 σ2. Proof. `````` Ralf Jung committed Jan 25, 2016 100 101 `````` intros Hv ? Hs [i ?]%elem_of_list_lookup He. destruct (ht_adequacy_own Q e1 t2 σ1 m σ2) as (rs2&Qs&?&?); auto. `````` Robbert Krebbers committed Jan 20, 2016 102 103 `````` { by rewrite -(ht_mask_weaken E coPset_all). } destruct (Forall3_lookup_l (λ e Q r, wp coPset_all e Q 3 r) t2 `````` Robbert Krebbers committed Feb 10, 2016 104 `````` (Q :: Qs) rs2 i e2) as (Q'&r2&?&?&Hwp); auto. `````` Robbert Krebbers committed Jan 20, 2016 105 106 107 `````` destruct (wp_step_inv coPset_all ∅ Q' e2 2 3 σ2 r2 (big_op (delete i rs2))); rewrite ?right_id_L ?big_op_delete; auto. Qed. `````` Ralf Jung committed Jan 25, 2016 108 ``````Theorem ht_adequacy_safe E Q e1 t2 σ1 m σ2 : `````` Robbert Krebbers committed Feb 01, 2016 109 `````` ✓ m → `````` Ralf Jung committed Jan 25, 2016 110 `````` {{ ownP σ1 ★ ownG m }} e1 @ E {{ Q }} → `````` Robbert Krebbers committed Jan 20, 2016 111 112 113 114 115 116 `````` rtc step ([e1], σ1) (t2, σ2) → Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3). Proof. intros. destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|]. apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2). `````` Ralf Jung committed Jan 25, 2016 117 `````` destruct (ht_adequacy_reducible E Q e1 e2 t2 σ1 m σ2) as (e3&σ3&ef&?); `````` Robbert Krebbers committed Jan 20, 2016 118 119 120 121 122 `````` rewrite ?eq_None_not_Some; auto. destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto. right; exists (t2' ++ e3 :: t2'' ++ option_list ef), σ3; econstructor; eauto. Qed. End adequacy.``````