Commit 38546fc3 by Hai Dang

### complete retag public

parent d51d5e9b
 ... @@ -761,6 +761,27 @@ Proof. ... @@ -761,6 +761,27 @@ Proof. right; (split; [lia|done]). right; (split; [lia|done]). Qed. Qed. Lemma retag_change_tag α cids c nxtp l otag ntag rk pk T α' nxtp' : retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') → ntag = otag ∨ match ntag with | Tagged t => t = nxtp ∧ nxtp' = S nxtp | _ => True end. Proof. intros RT. destruct (retag_change_case _ _ _ _ _ _ _ _ _ _ _ _ RT) as [[?[?[??]]]|[? Eq]]. - simplify_eq; by left. - destruct pk. + apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag. + destruct rk. * left. by destruct Eq as [_ []]; subst. * left. by destruct Eq as [_ []]; subst. * apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag. * left. by destruct Eq as [_ []]; subst. + apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag. Qed. Lemma retag_change_nxtp α cids c nxtp l otag ntag rk pk T α' nxtp' : Lemma retag_change_nxtp α cids c nxtp l otag ntag rk pk T α' nxtp' : retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') → retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') → (nxtp ≤ nxtp')%nat. (nxtp ≤ nxtp')%nat. ... @@ -1546,3 +1567,90 @@ Proof. ... @@ -1546,3 +1567,90 @@ Proof. case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq. case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq. move : GR. eapply grant_head_preserving; eauto. move : GR. eapply grant_head_preserving; eauto. Qed. Qed. Lemma grant_active_SRW stk old it cids stk' it' (SRW: it.(perm) = SharedReadWrite) : grant stk old it cids = Some stk' → it' ∈ stk → it' ∈ stk'. Proof. rewrite /grant. case find_granting as [[n p]|]; [|done]. rewrite /= SRW. case find_first_write_incompatible as [n'|]; [|done]. rewrite /= => ?. simplify_eq. destruct (item_insert_dedup_case stk it n') as [EQ|EQ]; rewrite EQ; [|done]. rewrite -{1}(take_drop n' stk). set_solver. Qed. Lemma grant_active_non_SRW stk old it cids stk' t pm c (SRW: it.(perm) ≠ SharedReadWrite) (Inc: c ∈ cids) : grant stk old it cids = Some stk' → let it' := mkItem pm t (Some c) in it' ∈ stk → it' ∈ stk'. Proof. rewrite /grant. case find_granting as [[n p]|] eqn:FR; [|done]. case it.(perm) eqn:Eqp; [|done|..|]; cbn -[item_insert_dedup]; (case access1 as [[n' stk1]|] eqn:ACC; [|done]); cbn -[item_insert_dedup]; intros ?; simplify_eq; move => /(access1_active_preserving _ _ _ _ _ _ ACC _ _ _ Inc); (destruct (item_insert_dedup_case stk1 it O) as [EQ|EQ]; rewrite EQ; [|done]); rewrite -{1}(take_drop 0 stk1); set_solver. Qed. Lemma grant_active_preserving stk old it cids stk' t pm c (Inc: c ∈ cids) : grant stk old it cids = Some stk' → let it' := mkItem pm t (Some c) in it' ∈ stk → it' ∈ stk'. Proof. case (decide (it.(perm) = SharedReadWrite)) => ?. - by apply grant_active_SRW. - by eapply grant_active_non_SRW. Qed. Lemma retag_item_active_preserving α nxtp c cids l old rk pk T new α' nxtp' : retag α nxtp cids c l old rk pk T = Some (new, α', nxtp') → ∀ l' stk t' c' pm, α !! l' = Some stk → c' ∈ cids → let it' := mkItem pm t' (Some c') in it' ∈ stk → ∃ stk', α' !! l' = Some stk' ∧ it' ∈ stk'. Proof. intros RT l' stk t' c' pm Eqstk Inc' it' IN. destruct (retag_Some _ _ _ _ _ _ _ _ _ _ _ _ RT) as [NEQ EQ]. destruct (block_case l l' (tsize T)) as [?|(i & Lti & ?)]. { rewrite NEQ //. naive_solver. } assert (∃ sz, tsize T = S sz) as [sz Eqsz]. { destruct (tsize T); [lia|by eexists]. } subst l'. move : RT. rewrite /retag /= /retag_ref Eqsz. destruct pk as [[]|[]|]. - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq. case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq. exists stk2. split; [done|]. move : Inc' GR IN. by apply grant_active_preserving. - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & b & GR). simplify_eq. case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq. exists stk2. split; [done|]. move : Inc' GR IN. by apply grant_active_preserving. - destruct rk; [by intros; simplify_eq; naive_solver..| |intros; simplify_eq; naive_solver]. specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq. case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq. exists stk2. split; [done|]. move : Inc' GR IN. by apply grant_active_preserving. - destruct rk; [by intros; simplify_eq; naive_solver..| |intros; simplify_eq; naive_solver]. specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & b & GR). simplify_eq. case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq. exists stk2. split; [done|]. move : Inc' GR IN. by apply grant_active_preserving. - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq. case reborrow as [α1|]; [|done]. simpl. intros ?. simplify_eq. exists stk2. split; [done|]. move : Inc' GR IN. by apply grant_active_preserving. Qed.
 ... @@ -293,6 +293,18 @@ Proof. ... @@ -293,6 +293,18 @@ Proof. by apply cmra_included_r. by apply cmra_included_r. Qed. Qed. Lemma tmap_lookup_op_l_equiv_pub (pm1 pm2: tmapUR) t h1 (VALID: ✓ (pm1 ⋅ pm2)): pm1 !! t ≡ Some (to_tgkR tkPub, h1) → ∃ h2, (pm1 ⋅ pm2) !! t ≡ Some (to_tgkR tkPub, h1 ⋅ h2). Proof. intros HL. move : (VALID t). rewrite lookup_op. destruct (pm2 !! t) as [[k2 h2]|] eqn:Eqt; rewrite Eqt; rewrite -> HL. - rewrite -Some_op pair_op. move => [ VL1 ?]. exists h2. simpl in VL1. rewrite HL -Some_op pair_op. by rewrite -(tagKindR_incl_eq (to_tgkR tkPub) _ VL1 (cmra_included_r _ _)). - intros _. exists (∅: gmap loc _). by rewrite 2!right_id HL. Qed. Lemma tmap_lookup_op_r_equiv_pub (pm1 pm2: tmapUR) t h2 Lemma tmap_lookup_op_r_equiv_pub (pm1 pm2: tmapUR) t h2 (VALID: ✓ (pm1 ⋅ pm2)): (VALID: ✓ (pm1 ⋅ pm2)): ... ...
 ... @@ -297,8 +297,8 @@ Proof using Type*. ... @@ -297,8 +297,8 @@ Proof using Type*. sim_bind (subst_map _ e) (subst_map _ e). sim_bind (subst_map _ e) (subst_map _ e). eapply sim_simple_post_mono, IHe; [|by auto..]. eapply sim_simple_post_mono, IHe; [|by auto..]. intros r' n' rs rt (-> & Hrel). simpl. intros r' n' rs rt (-> & Hrel). simpl. eapply sim_simple_retag_public; eauto. eapply sim_simple_valid_post. split; first done. constructor; done. by eapply sim_simple_retag_public; eauto. - (* Let *) - (* Let *) move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1). move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1). eapply sim_simple_frame_core. eapply sim_simple_frame_core. ... ...
 ... @@ -1206,13 +1206,14 @@ Qed. ... @@ -1206,13 +1206,14 @@ Qed. (** Retag *) (** Retag *) Lemma sim_body_retag_public fs ft r n ptr pk T kind σs σt Φ Lemma sim_body_retag_public fs ft r n ptr pk T kind σs σt Φ (RREL: rrel r ptr ptr) : (RREL: rrel r ptr ptr) : (∀ l otg ntg α' nxtp' c cids, (∀ l otg ntg α' nxtp' c cids r', ptr = ValR [ScPtr l otg] → ptr = ValR [ScPtr l otg] → σt.(scs) = c :: cids → σt.(scs) = c :: cids → retag σt.(sst) σt.(snp) σt.(scs) c l otg kind pk T = Some (ntg, α', nxtp') → retag σt.(sst) σt.(snp) σt.(scs) c l otg kind pk T = Some (ntg, α', nxtp') → vrel (r ⋅ r') [ScPtr l ntg] [ScPtr l ntg] → let σs' := mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc) in let σs' := mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc) in let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in Φ r n (ValR [ScPtr l ntg]) σs' (ValR [ScPtr l ntg]) σt') → Φ (r ⋅ r') n (ValR [ScPtr l ntg]) σs' (ValR [ScPtr l ntg]) σt') → r ⊨{n,fs,ft} r ⊨{n,fs,ft} (Retag ptr pk T kind, σs) ≥ (Retag ptr pk T kind, σs) ≥ (Retag ptr pk T kind, σt) : Φ. (Retag ptr pk T kind, σt) : Φ. ... @@ -1250,20 +1251,65 @@ Proof. ... @@ -1250,20 +1251,65 @@ Proof. - rewrite Eqcs; eauto. - rewrite Eqcs; eauto. - by rewrite Eqsst Eqnp Eqcs. } - by rewrite Eqsst Eqnp Eqcs. } exists (#[ScPtr l ntg])%V, σs', r, n. subst σt'. have HNP := wsat_tmap_nxtp _ _ _ WSAT1. split; last split. have Eqtg := retag_change_tag _ _ _ _ _ _ _ _ _ _ _ _ EqRT. { left. by constructor. } set r' : resUR := if (decide (ntg = otg)) then ε else { (* unfolding rrel for place *) match ntg with | Tagged t => res_tag t tkPub ∅ | _ => ε end. have VALID': ✓ (r_f ⋅ r ⋅ r'). { rewrite /r'. case decide => ?; [by rewrite right_id|]. destruct Eqtg as [|Eqtg]; [by subst|]. destruct ntg; [destruct Eqtg; subst t|by rewrite right_id]. apply (local_update_discrete_valid_frame (r_f ⋅ r) ε); [by rewrite right_id|]. rewrite right_id. by apply res_tag_alloc_local_update. } have Eqc': (r_f ⋅ r ⋅ r').(rcm) ≡ (r_f ⋅ r).(rcm). { rewrite /r'. case decide => ?; [by rewrite right_id|]. destruct ntg; by rewrite /= right_id. } have HLt: ∀ t kh, (r_f ⋅ r).(rtm) !! t ≡ Some kh → (r_f ⋅ r ⋅ r').(rtm) !! t ≡ Some kh. { intros t kh Eqt. rewrite /r'. case decide => ?; [by rewrite right_id|]. destruct Eqtg as [|Eqtg]; [by subst|]. destruct ntg as [t1|]; [destruct Eqtg; subst t1 nxtp'|by rewrite right_id]. rewrite lookup_op res_tag_lookup_ne. - by rewrite right_id. - intros ?. subst t. rewrite HNP in Eqt. inversion Eqt. } (* unfolding rrel for place *) simpl in RREL. simpl in RREL. inversion RREL as [|???? AREL _]; subst; simplify_eq. clear RREL. inversion RREL as [|???? AREL _]; subst; simplify_eq. clear RREL. have Lenp: (σt.(snp) ≤ nxtp')%nat by apply retag_change_nxtp in EqRT. exists (#[ScPtr l ntg])%V, σs', (r ⋅ r'), n. split; last split. { left. by constructor. } { have Lenp: (σt.(snp) ≤ nxtp')%nat by apply retag_change_nxtp in EqRT. split; last split; last split; last split; last split. split; last split; last split; last split; last split. - by apply (tstep_wf _ _ _ STEPS WFS). - by apply (tstep_wf _ _ _ STEPS WFS). - by apply (tstep_wf _ _ _ STEPT WFT). - by apply (tstep_wf _ _ _ STEPT WFT). - done. - by rewrite cmra_assoc. - intros t' k' h' Eqt'. - intros t' k' h' Eqt'. specialize (PINV _ _ _ Eqt') as [Ltp PINV]. have Eqh': (r_f ⋅ r).(rtm) !! t' ≡ Some (to_tgkR k', h') ∨ t' = σt.(snp) ∧ nxtp' = S σt.(snp) ∧ h' ≡ ∅. { move : Eqt'. rewrite /r'. case decide => ?; [by rewrite right_id; left|]. destruct Eqtg as [|Eqtg]; [by subst|]. destruct ntg as [t1|]; [destruct Eqtg; subst t1 nxtp'|by rewrite right_id; left]. rewrite cmra_assoc lookup_op. case (decide (t' = σt.(snp))) => ?; [subst t'|]. - rewrite res_tag_lookup. rewrite HNP left_id fmap_empty. intros [Eq1 Eq2]%Some_equiv_inj. by right. - rewrite res_tag_lookup_ne // right_id. by left. } destruct Eqh' as [Eqt|(?&?&Eqh')]; last first. { subst t' nxtp'. split; [simpl; lia|]. intros l' ss st. rewrite Eqh' lookup_empty. by inversion 1. } specialize (PINV _ _ _ Eqt) as [Ltp PINV]. split; [by simpl; lia|]. split; [by simpl; lia|]. intros l1 ss st Eql1 PRE. specialize (PINV _ _ _ Eql1). intros l1 ss st Eql1 PRE. specialize (PINV _ _ _ Eql1). destruct k'. destruct k'. ... @@ -1272,7 +1318,7 @@ Proof. ... @@ -1272,7 +1318,7 @@ Proof. have NEq: otg ≠ Tagged t'. have NEq: otg ≠ Tagged t'. { intros ?. subst otg. simpl in AREL. { intros ?. subst otg. simpl in AREL. destruct AREL as (_ & _ & ht & Eqh'). destruct AREL as (_ & _ & ht & Eqh'). move : Eqt'. rewrite lookup_op Eqh'. move : Eqt. rewrite lookup_op Eqh'. apply tagKindR_local_exclusive_r. } apply tagKindR_local_exclusive_r. } move : NEq Eqstk. move : NEq Eqstk. by eapply retag_Some_local. by eapply retag_Some_local. ... @@ -1293,7 +1339,7 @@ Proof. ... @@ -1293,7 +1339,7 @@ Proof. have NEq: Tagged t' ≠ otg. have NEq: Tagged t' ≠ otg. { intros ?. subst otg. simpl in AREL. { intros ?. subst otg. simpl in AREL. destruct AREL as (_ & _ & ht & Eqh'). destruct AREL as (_ & _ & ht & Eqh'). move : Eqt'. rewrite lookup_op Eqh'. move : Eqt. rewrite lookup_op Eqh'. apply tagKindR_uniq_exclusive_r. } apply tagKindR_uniq_exclusive_r. } move : HTOP. move : HTOP. by apply (retag_item_head_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT by apply (retag_item_head_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT ... @@ -1310,21 +1356,38 @@ Proof. ... @@ -1310,21 +1356,38 @@ Proof. have ND2 := proj2 (state_wf_stack_item _ WFT _ _ Eqstk1). have ND2 := proj2 (state_wf_stack_item _ WFT _ _ Eqstk1). by apply (retag_item_active_SRO_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT by apply (retag_item_active_SRO_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT _ _ _ _ _ ND2 Eqstk1 Eqstk' In In'). _ _ _ _ _ ND2 Eqstk1 Eqstk' In In'). - intros c1 Tc Eqc. specialize (CINV _ _ Eqc) as [Ltc CINV]. - intros c1 Tc. rewrite cmra_assoc Eqc'. intros Eqc. specialize (CINV _ _ Eqc) as [Ltc CINV]. split; [done|]. split; [done|]. intros tc L EqL. specialize (CINV _ _ EqL) as [Ltp CINV]. intros tc L EqL. specialize (CINV _ _ EqL) as [Ltp CINV]. split; [by simpl; lia|]. split; [by simpl; lia|]. intros l1 InL. simpl. intros l1 InL. simpl. specialize (CINV _ InL) as (stk & pm & Eqstk & In & NDIS). specialize (CINV _ InL) as (stk & pm & Eqstk & In & NDIS). (* Prove that this is active (protector) preserving *) destruct (retag_item_active_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT (* destruct (retag_item_in _ _ _ _ _ _ _ _ _ _ _ _ EqRT _ _ t' _ Eqstk' In') _ _ _ _ _ Eqstk Ltc In) as (stk' & Eqstk' & In'). as (stk & Eqstk & In); [done..|]. *) by exists stk', pm. admit. - rewrite cmra_assoc. do 4 (split; [done|]). - done. } move => l' /PUBP [PB|PV]. + left. move => ? /PB [? [? AREL']]. eexists. split; [done|]. eapply arel_mono; [done|..|exact AREL']. apply cmra_included_l. + right. destruct PV as (t & k1 & h1 & Eqt & ?). exists t, k1, h1. setoid_rewrite Eqc'. split; [|done]. by apply HLt. } left. left. apply: sim_body_result. intros. eapply POST; eauto. apply: sim_body_result. intros VALIDr. eapply POST; eauto. Abort. constructor; [|done]. do 2 (split; [done|]). destruct ntg; [|done]. destruct AREL as (_ & _ & AREL). rewrite /r'. case decide => ?; [subst otg|]. - destruct AREL as [h1 ?]. exists h1. by rewrite right_id. - destruct Eqtg as [|[]]; [by subst otg|subst t]. destruct (tmap_lookup_op_r_equiv_pub r.(rtm) (res_tag σt.(snp) tkPub ∅).(rtm) σt.(snp) (to_agree <\$> ∅)). + move : VALIDr. rewrite /r' decide_False // => VALIDr. apply VALIDr. + apply res_tag_lookup. + by eexists. Qed. Lemma sim_body_retag_mut_ref_default fs ft r r' rs n l told T σs σt Φ : Lemma sim_body_retag_mut_ref_default fs ft r r' rs n l told T σs σt Φ : (0 < tsize T)%nat → (0 < tsize T)%nat → ... ...
 ... @@ -385,11 +385,14 @@ Qed. ... @@ -385,11 +385,14 @@ Qed. Lemma sim_simple_retag_public fs ft r n (rs rt: result) pk T rk Φ : Lemma sim_simple_retag_public fs ft r n (rs rt: result) pk T rk Φ : rrel r rs rt → rrel r rs rt → (Φ r n (ValR [☠%S]) (ValR [☠%S])) → (∀ l old new rt, rs = ValR [ScPtr l old] → vrel (r ⋅ rt) [ScPtr l new] [ScPtr l new] → Φ (r ⋅ rt) n (ValR [ScPtr l new]) (ValR [ScPtr l new])) → r ⊨ˢ{n,fs,ft} Retag rs pk T rk ≥ Retag rt pk T rk : Φ. r ⊨ˢ{n,fs,ft} Retag rs pk T rk ≥ Retag rt pk T rk : Φ. Proof. Proof. intros [Hrel ?]%rrel_with_eq. simplify_eq. intros [Hrel ?]%rrel_with_eq HH σs σt. simplify_eq. Admitted. eapply sim_body_retag_public; eauto. Qed. (** * Pure *) (** * Pure *) Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 Φ : Lemma sim_simple_let fs ft r n x (vs1 vt1: result) es1 et1 es2 et2 Φ : ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!