Commit 5714f22b by Hai Dang

### fix write local and simple

parent 2bc85deb
 ... ... @@ -1176,6 +1176,69 @@ Proof. eapply retag1_head_step'; eauto. Qed. Lemma retag_ref_change_1 h α cids c nxtp x rk mut T h' α' nxtp' (N2: rk ≠ TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp') → ∃ l otag, h !! x = Some (ScPtr l otag) ∧ ∃ rk' new, h' = <[x := ScPtr l new]>h ∧ retag_ref h α cids nxtp l otag T rk' (adding_protector rk c) = Some (new, α', nxtp') ∧ rk' = if mut then UniqueRef (is_two_phase rk) else SharedRef. Proof. rewrite retag_equation_2 /=. destruct (h !! x) as [[| |l t|]|]; simpl; [done..| |done|done]. destruct mut; (case retag_ref as [[[t1 α1] n1]|] eqn:Eq => [/=|//]); intros; simplify_eq; exists l, t; (split; [done|]); eexists; exists t1; done. Qed. Lemma retag_ref_change_2 h α cids c nxtp l otag rk (mut: mutability) T new α' nxtp' (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : let rk' := if mut then UniqueRef false else SharedRef in let opro := (adding_protector rk c) in retag_ref h α cids nxtp l otag T rk' opro = Some (new, α', nxtp') → nxtp' = S nxtp ∧ new = Tagged nxtp ∧ reborrowN α cids l (tsize T) otag (Tagged nxtp) (if mut then Unique else SharedReadOnly) opro = Some α'. Proof. intros rk' opro. rewrite /retag_ref. destruct (tsize T) as [|n] eqn:EqT; [lia|]. destruct mut; simpl; [|rewrite visit_freeze_sensitive_is_freeze //]; case reborrowN as [α1|] eqn:Eq1 => [/=|//]; intros; simplify_eq; by rewrite -EqT. Qed. Lemma retag_ref_change h α cids c nxtp x rk mut T h' α' nxtp' (N2: rk ≠ TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp') → ∃ l otag, h !! x = Some (ScPtr l otag) ∧ h' = <[x := ScPtr l (Tagged nxtp)]>h ∧ nxtp' = S nxtp ∧ reborrowN α cids l (tsize T) otag (Tagged nxtp) (if mut then Unique else SharedReadOnly) (adding_protector rk c) = Some α'. Proof. intros RT. apply retag_ref_change_1 in RT as (l & otag & EqL & rk' & new & Eqh & RT &?); [|done..]. subst. exists l, otag. split; [done|]. rewrite (_: is_two_phase rk = false) in RT; [|by destruct rk]. apply retag_ref_change_2 in RT as (?&?&?); [|done..]. by subst new. Qed. Lemma retag_ref_reborrowN (h: mem) α t cids c x l otg T rk (mut: mutability) α' (N2: rk ≠ TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : h !! x = Some (ScPtr l otg) → reborrowN α cids l (tsize T) otg (Tagged t) (if mut then Unique else SharedReadOnly) (adding_protector rk c) = Some α' → retag h α t cids c x rk (Reference (RefPtr mut) T) = Some (<[x:=ScPtr l (Tagged t)]> h, α', S t). Proof. intros Eqx RB. rewrite retag_equation_2 Eqx /= /retag_ref. destruct (tsize T) eqn:EqT; [lia|]. rewrite (_: is_two_phase rk = false); [|by destruct rk]. destruct mut; simpl; [|rewrite visit_freeze_sensitive_is_freeze //]; rewrite EqT RB /= //. Qed. (* Lemma syscall_head_step σ id : head_step (SysCall id) σ [SysCallEvt id] #☠ σ []. ... ...
 ... ... @@ -92,7 +92,7 @@ Proof. { rewrite lookup_insert. done. } (* Finishing up. *) eapply sim_body_viewshift. { do 6 eapply viewshift_frame_r. eapply vs_call_empty_public. } { do 5 eapply viewshift_frame_r. eapply vs_call_empty_public. } apply: sim_body_result=>Hval. simpl. split. - eexists. split; first done. eapply res_end_call_sat; first done. solve_res. ... ...
 ... ... @@ -99,8 +99,11 @@ Proof. Qed. Lemma tagKindR_exclusive_heaplet (h0 h: heapletR) mb : mb ⋅ Some (to_tagKindR tkUnique, h0) ≡ Some (to_tagKindR tkUnique, h) → h0 ≡ h. Proof. by intros []%tagKindR_exclusive_heaplet'. Qed. Some mb ⋅ Some (to_tagKindR tkUnique, h0) ≡ Some (to_tagKindR tkUnique, h) → False. Proof. destruct mb as [c ]. rewrite -Some_op pair_op. intros [Eq _]%Some_equiv_inj. destruct c; inversion Eq; simpl in *; simplify_eq. Qed. Lemma tagKindR_valid (k: tagKindR) : valid k → ∃ k', k = to_tagKindR k'. ... ... @@ -220,6 +223,15 @@ Proof. rewrite -Some_op pair_op. intros [?%exclusive_r]; [done|apply _]. Qed. Lemma tmap_lookup_op_r_unique_equiv (pm1 pm2: tmapUR) t h0 (VALID: ✓ (pm1 ⋅ pm2)): pm2 !! t ≡ Some (to_tagKindR tkUnique, h0) → (pm1 ⋅ pm2) !! t ≡ Some (to_tagKindR tkUnique, h0). Proof. intros HL. move : (VALID t). rewrite lookup_op HL. destruct (pm1 !! t) as [[k1 h1]|] eqn:Eqt; rewrite Eqt; [|done]. rewrite -Some_op pair_op. intros [?%exclusive_r]; [done|apply _]. Qed. Lemma tmap_lookup_op_l_unique_equiv (pm1 pm2: tmapUR) t h0 (VALID: ✓ (pm1 ⋅ pm2)): pm1 !! t ≡ Some (to_tagKindR tkUnique, h0) → ... ... @@ -455,6 +467,14 @@ Proof. naive_solver. Qed. Lemma res_mapsto_llookup_1 l v t (LEN: (0 < length v)%nat) : ((res_mapsto l v t).(rlm) !! l : optionR tagR) ≡ Some (to_tagR t). Proof. rewrite lookup_op /= lookup_empty right_id lookup_fmap. destruct (length v); [lia|]. rewrite /= lookup_insert //. Qed. Lemma res_mapsto_tlookup l v (t: ptr_id) : (res_mapsto l v t).(rtm) !! t ≡ Some (to_tagKindR tkUnique, to_agree <\$> (write_mem l v ∅)). ... ...
 ... ... @@ -287,3 +287,15 @@ Proof. intros Hrel. eapply Forall2_impl; first done. eauto using vrel_persistent. Qed. Lemma arel_res_mapsto_overwrite_1 r l t v1 v2 ss st : arel (r ⋅ res_mapsto l [v1] t) ss st → arel (r ⋅ res_mapsto l [v2] t) ss st. Proof. destruct ss as [| |? [t1|]|], st as [| |? []|]; simpl; auto; [|naive_solver]. intros (?&?& h & Eqh). do 2 (split; [done|]). case (decide (t1 = t)) => ?; [subst t1|]. - exfalso. move : Eqh. rewrite lookup_op res_mapsto_tlookup. apply tagKindR_exclusive. - exists h. move : Eqh. by do 2 (rewrite lookup_op res_mapsto_tlookup_ne; [|done]). Qed.
 ... ... @@ -391,7 +391,7 @@ Lemma sim_body_copy_public fs ft r n (pl: result) σs σt Φ ∀ α', memory_read σt.(sst) σt.(scs) l t (tsize T) = Some α' → let σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc) in let σt' := mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc) in vrel (r ⋅ r') vs vt → Φ (r ⋅ r') n (ValR vs) σs' (ValR vt) σt') → vrel ((* r ⋅ *) r') vs vt → Φ (r ⋅ r') n (ValR vs) σs' (ValR vt) σt') → r ⊨{n,fs,ft} (Copy pl, σs) ≥ (Copy pl, σt) : Φ. Proof. intros POST. pfold. intros NT. intros. ... ... @@ -504,10 +504,7 @@ Proof. destruct (local_access_eq _ _ _ _ _ _ _ _ _ _ Eqst ACC1 WSAT1 Eqs) as [? Eqstk2]. by rewrite Eq2 Eqstk2. } left. apply: sim_body_result. intros. have VREL2: vrel (r ⋅ (core (r_f ⋅ r))) vs vt. { eapply vrel_mono; [done| |exact VREL']. apply cmra_included_r. } eapply POST; eauto. apply: sim_body_result. intros. eapply POST; eauto. Qed. (** Write *) ... ... @@ -624,16 +621,22 @@ Proof. { rewrite LenT in EQL. destruct v as [|s v]; [simpl in EQL; done|]. exists s. destruct v; [done|simpl in EQL; lia]. } subst v. have VALIDr:= cmra_valid_op_r _ _ VALID. have HLlr: r.(rlm) !! l ≡ Some (to_locStateR (lsLocal v' tg)). { rewrite Eqr. apply lmap_lookup_op_r. - rewrite ->Eqr in VALIDr. apply VALIDr. - by rewrite /= /init_local_res lookup_fmap /= lookup_insert /=. } destruct (LINV l v' tg) as (Eql1 & Eql2 & Eqsl1 & Eqsl2 & LocUnique). have VALIDr:= cmra_valid_op_r _ _ VALID. rewrite ->Eqr in VALIDr. have HLlr: (r.(rlm) !! l : optionR tagR) ≡ Some (to_tagR tg). { rewrite Eqr. apply (lmap_lookup_op_included (res_mapsto l [v'] tg).(rlm)). - apply VALIDr. - apply cmra_included_r. - apply res_mapsto_llookup_1. simpl; lia. } have HLtr: r.(rtm) !! tg ≡ Some (to_tagKindR tkUnique, {[l := to_agree v']}). { rewrite Eqr. eapply tmap_lookup_op_unique_included; [apply VALIDr|apply cmra_included_r|]. rewrite res_mapsto_tlookup /= fmap_insert fmap_empty //. } destruct (LINV l tg) as (Lte & Eql2 & Eqh2). { apply lmap_lookup_op_r; [apply VALID|done]. } have ?: α' = σt.(sst). { move : Eqα'. rewrite LenT /= /memory_written /= shift_loc_0_nat. rewrite Eqsl2 /=. { move : Eqα'. rewrite LenT /= /memory_written /= shift_loc_0_nat Eql2 /=. destruct (tag_unique_head_access σt.(scs) (init_stack (Tagged tg)) tg None AccessWrite) as [ns Eqss]; [by exists []|]. rewrite Eqss /= insert_id //. by inversion 1. } subst α'. ... ... @@ -646,90 +649,125 @@ Proof. rewrite EQL in EqD. rewrite -Eqnp in IN. eapply (head_step_fill_tstep _ []), write_head_step'; eauto. } exists (#[☠])%V, σs', (r' ⋅ res_mapsto l 1 s tg), n. exists (#[☠])%V, σs', (r' ⋅ res_mapsto l [s] tg), n. split; last split. { left. by constructor 1. } { have HLlrf: (r_f ⋅ r) .(rlm) !! l ≡ Some (to_locStateR (lsLocal v' tg)). { have HLlrf: ((r_f ⋅ r) .(rlm) !! l : optionR tagR) ≡ Some \$ to_tagR tg. { apply lmap_lookup_op_r; [apply VALID|done]. } have HLN: (r_f ⋅ r').(rlm) !! l = None. { destruct ((r_f ⋅ r').(rlm) !! l) as [ls|] eqn:Eqls; [|done]. exfalso. move : HLlrf. rewrite Eqr cmra_assoc lookup_op Eqls /= /init_local_res lookup_fmap /= lookup_insert. apply lmap_exclusive_2. } have HTEq: (r_f ⋅ r' ⋅ res_mapsto l 1 v' tg).(rtm) ≡ (r_f ⋅ r' ⋅ res_mapsto l 1 s tg).(rtm). { rewrite /rtm /= right_id //. } have HCEq: (r_f ⋅ r' ⋅ res_mapsto l 1 v' tg).(rcm) ≡ (r_f ⋅ r' ⋅ res_mapsto l 1 s tg).(rcm). rewrite Eqr cmra_assoc lookup_op Eqls (res_mapsto_llookup_1 l [v'] tg). - apply lmap_exclusive_2. - simpl; lia. } have HLtrf: (r_f ⋅ r) .(rtm) !! tg ≡ Some (to_tagKindR tkUnique, {[l := to_agree v']}). { apply tmap_lookup_op_r_unique_equiv; [apply VALID|done]. } have HLNt: (r_f ⋅ r').(rtm) !! tg = None. { destruct ((r_f ⋅ r').(rtm) !! tg) as [ls|] eqn:Eqls; [|done]. exfalso. move : HLtrf. rewrite Eqr cmra_assoc lookup_op Eqls res_mapsto_tlookup. apply tagKindR_exclusive_heaplet. } (* have HTEq: (r_f ⋅ r' ⋅ res_mapsto l [v'] tg).(rtm) ≡ (r_f ⋅ r' ⋅ res_mapsto l [s] tg).(rtm). *) have HCEq : (r_f ⋅ r' ⋅ res_mapsto l [v'] tg).(rcm) ≡ (r_f ⋅ r' ⋅ res_mapsto l [s] tg).(rcm). { rewrite /rcm /= right_id //. } have HLtg: (r_f ⋅ r' ⋅ res_mapsto l [s] tg).(rtm) !! tg ≡ Some (to_tagKindR tkUnique, {[l := to_agree s]}). { rewrite lookup_op HLNt left_id res_mapsto_tlookup fmap_insert fmap_empty //. } rewrite cmra_assoc. have VALID' : ✓ (r_f ⋅ r' ⋅ res_mapsto l [s] tg). { move : VALID. rewrite Eqr cmra_assoc => VALID. apply (local_update_discrete_valid_frame _ _ _ VALID). by eapply res_mapsto_1_insert_local_update. } split; last split; last split; last split; last split; last split. - by apply (tstep_wf _ _ _ STEPS WFS). - by apply (tstep_wf _ _ _ STEPT WFT). - move : VALID. rewrite Eqr cmra_assoc => VALID. apply (local_update_discrete_valid_frame _ _ _ VALID). by eapply res_mapsto_1_insert_local_update. - intros t k h HL. destruct (PINV t k h) as [? PI]. { rewrite Eqr. move: HL. by rewrite 4!lookup_op /= 2!right_id. } split; [done|]. simpl. intros l1 s1 Eqs1. specialize (PI l1 s1 Eqs1) as [HLs1 PI]. have NEql1: l1 ≠ l. { intros ?. subst l1. move : HLs1. rewrite HLlrf. intros Eq%Some_equiv_inj. inversion Eq. } split. { move : HLs1. rewrite Eqr cmra_assoc /=. rewrite lookup_op (lookup_op (r_f.2 ⋅ r'.2)) /init_local_res /= 2!lookup_fmap. do 2 rewrite lookup_insert_ne //. } by setoid_rewrite lookup_insert_ne. - done. - intros t k h HL. simpl. case (decide (t = tg)) => ?; [subst t|]. + specialize (PINV _ _ _ HLtrf) as [? PINV]. split; [done|]. move : HL. rewrite HLtg. intros [Eq1 Eq2]%Some_equiv_inj. simpl in Eq1, Eq2. simplify_eq. intros l1 s1. rewrite -Eq2. case (decide (l1 = l)) => ?; [subst l1| rewrite lookup_insert_ne //; by inversion 1]. rewrite lookup_insert. intros Eq%Some_equiv_inj%to_agree_inj. symmetry in Eq. intros stk Eqstk. rewrite Eqstk in Eql2. simplify_eq. intros pm opro Inp%elem_of_list_singleton NDIS. split; [by rewrite lookup_insert|]. simplify_eq. destruct k; [|by inversion Eq1]. by exists []. + have HL': (r_f ⋅ r).(rtm) !! t ≡ Some (to_tagKindR k, h). { rewrite Eqr cmra_assoc. move: HL. rewrite lookup_op res_mapsto_tlookup_ne //. rewrite (lookup_op _ (res_mapsto _ _ _).(rtm)) res_mapsto_tlookup_ne //. } specialize (PINV _ _ _ HL') as [? PINV]. split; [done|]. intros l1 s1 Eqs1 stk Eqstk. case (decide (l1 = l)) => ?; [subst l1; rewrite lookup_insert|rewrite lookup_insert_ne //]. * rewrite Eqstk in Eql2. simplify_eq. intros pm opro Inp%elem_of_list_singleton NDIS. simplify_eq. * by apply PINV. - intros c cs. simpl. rewrite -HCEq. intros Eqcm. move : CINV. rewrite Eqr cmra_assoc => CINV. specialize (CINV _ _ Eqcm). destruct cs as [[]| |]; [|done..]. destruct CINV as [? CINV]. split; [done|]. by setoid_rewrite <- HTEq. - destruct SREL as (?&?&?&?& EqDl & REL). do 4 (split; [done|]). simpl. split. { rewrite dom_insert EqDl Eqr cmra_assoc. clear. rewrite 2!(dom_op (r_f.2 ⋅ r'.2)) 2!init_local_res_mem_dom /= insert_empty dom_singleton. set_solver. } intros l1 Eq1. have NEql1: l1 ≠ l. { intros ?. subst l1. move : Eq1. rewrite lookup_op HLN left_id. rewrite /init_local_res lookup_fmap /= lookup_insert. intros Eq%Some_equiv_inj. inversion Eq. } (* move : Inl1. rewrite dom_insert elem_of_union elem_of_singleton. intros [?|Inl1]; [done|]. *) have Eq1' : (r_f ⋅ r).(rlm) !! l1 ≡ Some (Cinr ()). { rewrite Eqr cmra_assoc -Eq1 lookup_op (lookup_op (r_f.2 ⋅ r'.2)). rewrite /init_local_res /= 2!lookup_fmap lookup_insert_ne // lookup_insert_ne //. } specialize (REL _ Eq1') as [REL|REL]. + left. move : REL. rewrite /pub_loc /=. do 2 rewrite lookup_insert_ne //. intros REL st Eqst. specialize (REL st Eqst) as [ss [Eqss AREL]]. exists ss. split; [done|]. move : AREL. rewrite /arel /=. destruct ss as [| |? [] |], st as [| |? []|]; try done; [|naive_solver]. setoid_rewrite Eqr. setoid_rewrite cmra_assoc. by setoid_rewrite <- HTEq. + right. move : REL. setoid_rewrite Eqr. setoid_rewrite cmra_assoc. rewrite /priv_loc. by setoid_rewrite <- HTEq. specialize (CINV _ _ Eqcm). destruct cs as [[Tc|]| |]; [|done..]. destruct CINV as [Inc CINV]. split; [done|]. intros t Int. specialize (CINV _ Int) as [Ltt CINV]. split; [done|]. intros k h. (* two private locs, one by protector, one by local *) (* TODO: extract? *) case (decide (t = tg)) => ?; [subst t|]. + exfalso. move : HLtrf. rewrite Eqr cmra_assoc. intros HLtrf. specialize (CINV _ _ HLtrf l) as (stk & pm & Eqst & Instk & ?). { by rewrite dom_singleton elem_of_singleton. } rewrite Eqst in Eql2. simplify_eq. clear -Instk. apply elem_of_list_singleton in Instk. simplify_eq. + intros HL. have HL': (r_f ⋅ r' ⋅ res_mapsto l [v'] tg).(rtm) !! t ≡ Some (k, h). { move : HL. rewrite lookup_op res_mapsto_tlookup_ne //. rewrite (lookup_op _ (res_mapsto _ _ _).(rtm)) res_mapsto_tlookup_ne //. } apply (CINV _ _ HL'). - destruct SREL as (?&?&?&?& REL). do 4 (split; [done|]). simpl. intros l1 Inl1. case (decide (l1 = l)) => ?; [subst l1|]. + right. eexists tg, _. split. { by rewrite HLtg. } left. apply lmap_lookup_op_r; [apply VALID'|]. rewrite (res_mapsto_llookup_1 l [s] tg) //. simpl; lia. + move : Inl1. rewrite dom_insert elem_of_union elem_of_singleton. intros [?|Inl1]; [done|]. specialize (REL _ Inl1) as [PB|[t PV]]; [left|right]. * move : PB. rewrite Eqr cmra_assoc /pub_loc /= lookup_insert_ne; [|done]. intros PB st Eqst. specialize (PB _ Eqst) as (ss & Eqss & AREL). exists ss. split; [by rewrite lookup_insert_ne|]. move : AREL. apply arel_res_mapsto_overwrite_1. * exists t. move : PV. rewrite Eqr cmra_assoc /priv_loc. intros (h & Eqh & PV). case (decide (t = tg)) => ?; [subst t|]. { eexists. rewrite HLtg. split; [eauto|]. move : HLtrf. rewrite Eqr cmra_assoc. rewrite Eqh. intros [_ Eqh']%Some_equiv_inj. simpl in Eqh'. destruct PV as [PV|(c & Tc & PV & ? & Inh)]; [left|right]. - move : PV. rewrite lookup_op /= right_id lookup_fmap insert_empty lookup_insert_ne //. - exfalso. move : Inh. rewrite Eqh' dom_singleton elem_of_singleton //. } { exists h. setoid_rewrite HCEq. split; [|destruct PV as [PB|PV]]. - move : Eqh. rewrite lookup_op res_mapsto_tlookup_ne; [|done]. rewrite (lookup_op _ (res_mapsto _ _ _).(rtm)) res_mapsto_tlookup_ne //. - left. move : PB. rewrite lookup_op /= right_id lookup_fmap insert_empty lookup_insert_ne //. - by right. } - move : LINV. rewrite Eqr cmra_assoc. (* TODO: general property of lmap_inv w.r.t to separable resource *) intros LINV l1 s1 t1. specialize (LINV l1 s1 t1). destruct ((r_f ⋅ r').(rlm) !! l1) as [ls1|] eqn:Eqls1. + have NEQ: l1 ≠ l. { intros ?. subst l1. by rewrite Eqls1 in HLN. } intros EQl1. have EQl1' : (r_f ⋅ r' ⋅ res_mapsto l 1 v' tg).(rlm) !! l1 ≡ Some (to_locStateR (lsLocal s1 t1)). { move : EQl1. rewrite lookup_op Eqls1 lookup_op Eqls1. rewrite /= /init_local_res 2!lookup_fmap /= lookup_insert_ne // lookup_insert_ne //. } specialize (LINV EQl1'). rewrite /= lookup_insert_ne // lookup_insert_ne //. + rewrite /= lookup_op Eqls1 left_id /init_local_res /= lookup_fmap. intros Eq. case (decide (l1 = l)) => ?; [subst l1|]. * move : Eq. rewrite 3!lookup_insert /=. intros Eq%Some_equiv_inj. simplify_eq. do 4 (split; [done|]). destruct LocUnique as [h1 Eqh1]. exists h1. by rewrite -HTEq -cmra_assoc -Eqr Eqh1. * exfalso. move : Eq. rewrite lookup_insert_ne // lookup_empty /=. by inversion 1. } intros LINV l1 t1 Eq1. simpl. specialize (LINV l1 t1 Eq1) as (?&?&?). do 2 (split; [done|]). case (decide (l1 = l)) => [->|?]; [rewrite 2!lookup_insert //|rewrite lookup_insert_ne// lookup_insert_ne//]. } left. apply: sim_body_result. intros. simpl. by apply POST. ... ... @@ -754,7 +792,7 @@ Lemma sim_body_write_related_values r ⊨{n,fs,ft} (Place l (Tagged tg) Ts <- #v, σs) ≥ (Place l (Tagged tg) Tt <- #v, σt) : Φ. Proof. intros rw Eqr rw' POST. pfold. intros NT. intros. (* intros rw Eqr rw' POST. pfold. intros NT. intros. have WSAT1 := WSAT. destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV). split; [|done|]. ... ... @@ -1062,7 +1100,7 @@ Proof. } left. apply: sim_body_result. intros. simpl. by apply POST. intros. simpl. by apply POST. *) Abort. ... ... @@ -1086,70 +1124,6 @@ Admitted. (** Retag *) Lemma retag_ref_change_1 h α cids c nxtp x rk mut T h' α' nxtp' (N2: rk ≠ TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp') → ∃ l otag, h !! x = Some (ScPtr l otag) ∧ ∃ rk' new, h' = <[x := ScPtr l new]>h ∧ retag_ref h α cids nxtp l otag T rk' (adding_protector rk c) = Some (new, α', nxtp') ∧ rk' = if mut then UniqueRef (is_two_phase rk) else SharedRef. Proof. rewrite retag_equation_2 /=. destruct (h !! x) as [[| |l t|]|]; simpl; [done..| |done|done]. destruct mut; (case retag_ref as [[[t1 α1] n1]|] eqn:Eq => [/=|//]); intros; simplify_eq; exists l, t; (split; [done|]); eexists; exists t1; done. Qed. Lemma retag_ref_change_2 h α cids c nxtp l otag rk (mut: mutability) T new α' nxtp' (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : let rk' := if mut then UniqueRef false else SharedRef in let opro := (adding_protector rk c) in retag_ref h α cids nxtp l otag T rk' opro = Some (new, α', nxtp') → nxtp' = S nxtp ∧ new = Tagged nxtp ∧ reborrowN α cids l (tsize T) otag (Tagged nxtp) (if mut then Unique else SharedReadOnly) opro = Some α'. Proof. intros rk' opro. rewrite /retag_ref. destruct (tsize T) as [|n] eqn:EqT; [lia|]. destruct mut; simpl; [|rewrite visit_freeze_sensitive_is_freeze //]; case reborrowN as [α1|] eqn:Eq1 => [/=|//]; intros; simplify_eq; by rewrite -EqT. Qed. Lemma retag_ref_change h α cids c nxtp x rk mut T h' α' nxtp' (N2: rk ≠ TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp') → ∃ l otag, h !! x = Some (ScPtr l otag) ∧ h' = <[x := ScPtr l (Tagged nxtp)]>h ∧ nxtp' = S nxtp ∧ reborrowN α cids l (tsize T) otag (Tagged nxtp) (if mut then Unique else SharedReadOnly) (adding_protector rk c) = Some α'. Proof. intros RT. apply retag_ref_change_1 in RT as (l & otag & EqL & rk' & new & Eqh & RT &?); [|done..]. subst. exists l, otag. split; [done|]. rewrite (_: is_two_phase rk = false) in RT; [|by destruct rk]. apply retag_ref_change_2 in RT as (?&?&?); [|done..]. by subst new. Qed. Lemma retag_ref_reborrowN (h: mem) α t cids c x l otg T rk (mut: mutability) α' (N2: rk ≠ TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) : h !! x = Some (ScPtr l otg) → reborrowN α cids l (tsize T) otg (Tagged t) (if mut then Unique else SharedReadOnly) (adding_protector rk c) = Some α' → retag h α t cids c x rk (Reference (RefPtr mut) T) = Some (<[x:=ScPtr l (Tagged t)]> h, α', S t). Proof. intros Eqx RB. rewrite retag_equation_2 Eqx /= /retag_ref. destruct (tsize T) eqn:EqT; [lia|]. rewrite (_: is_two_phase rk = false); [|by destruct rk]. destruct mut; simpl; [|rewrite visit_freeze_sensitive_is_freeze //]; rewrite EqT RB /= //. Qed. Lemma sim_body_retag_default fs ft r n x xtag mut T σs σt Φ (TS: (O < tsize T)%nat) (FRZ: is_freeze T) (Eqx: σs.(shp) = σt.(shp)) : let Tr := (Reference (RefPtr mut) T) in ... ...
 ... ... @@ -243,9 +243,8 @@ Qed. (** * Memory: local *) Lemma sim_simple_alloc_local fs ft r n T css cst Φ : (∀ (l: loc) (tg: nat), let rt := res_tag tg tkUnique ∅ in let r' := res_mapsto l (tsize T) ☠ tg in Φ (r ⋅ rt ⋅ r') n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst) → let r' := res_mapsto l (repeat ☠%S (tsize T)) tg in Φ (r ⋅ r') n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst) → r ⊨ˢ{n,fs,ft} (Alloc T, css) ≥ (Alloc T, cst) : Φ. Proof. intros HH σs σt <-<-. apply sim_body_alloc_local=>/=. exact: HH. ... ... @@ -253,8 +252,8 @@ Qed. Lemma sim_simple_write_local fs ft r r' n l tg ty v v' css cst Φ : tsize ty = 1%nat → r ≡ r' ⋅ res_mapsto l 1 v' tg → (∀ s, v = [s] → Φ (r' ⋅ res_mapsto l 1 s tg) n (ValR [☠%S]) css (ValR [☠%S]) cst) → r ≡ r' ⋅ res_mapsto l [v'] tg → (∀ s, v = [s] → Φ (r' ⋅ res_mapsto l [s] tg) n (ValR [☠%S]) css (ValR [☠%S]) cst) → r ⊨ˢ{n,fs,ft} (Place l (Tagged tg) ty <- #v, css) ≥ (Place l (Tagged tg) ty <- #v, cst) : Φ. ... ... @@ -262,7 +261,7 @@ Proof. intros Hty Hres HH σs σt <-<-. eapply sim_body_write_local_1; eauto. Qe Lemma sim_simple_copy_local_l fs ft r r' n l tg ty s et css cst Φ : tsize ty = 1%nat → r ≡ r' ⋅ res_mapsto l 1 s tg → r ≡ r' ⋅ res_mapsto l [s] tg → (r ⊨ˢ{n,fs,ft} (#[s], css) ≥ (et, cst) : Φ) → r ⊨ˢ{n,fs,ft} (Copy (Place l (Tagged tg) ty), css) ≥ (et, cst) ... ... @@ -274,7 +273,7 @@ Qed. Lemma sim_simple_copy_local_r fs ft r r' n l tg ty s es css cst Φ : tsize ty = 1%nat → r ≡ r' ⋅ res_mapsto l 1 s tg → r ≡ r' ⋅ res_mapsto l [s] tg → (r ⊨ˢ{n,fs,ft} (es, css) ≥ (#[s], cst) : Φ) → r ⊨ˢ{S n,fs,ft} (es, css) ≥ (Copy (Place l (Tagged tg) ty), cst) ... ... @@ -286,7 +285,7 @@ Qed. Lemma sim_simple_copy_local fs ft r r' n l tg ty s css cst Φ : tsize ty = 1%nat → r ≡ r' ⋅ res_mapsto l 1 s tg → r ≡ r' ⋅ res_mapsto l [s] tg → (r ⊨ˢ{n,fs,ft} (#[s], css) ≥ (#[s], cst) : Φ) → r ⊨ˢ{S n,fs,ft} (Copy (Place l (Tagged tg) ty), css) ≥ (Copy (Place l (Tagged tg) ty), cst) ... ... @@ -298,7 +297,7 @@ Proof. Qed. Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty css cst Φ : r ≡ r' ⋅ res_mapsto l 1 s tg → r ≡ r' ⋅ res_mapsto l [s] tg → arel rs s' s → r' ≡ r'' ⋅ rs → (∀ l_inner tg_inner hplt, ... ... @@ -310,7 +309,7 @@ Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg ty css cst Φ : end → *) let tk := tkUnique in is_Some (hplt !! l_inner) → Φ (r'' ⋅ rs ⋅ res_mapsto l 1 s_new tg ⋅ res_tag tg_inner tk hplt) n (ValR [☠%S]) css (ValR [☠%S]) cst) → Φ (r'' ⋅ rs ⋅ res_mapsto l [s_new] tg ⋅ res_tag tg_inner tk hplt) n (ValR [☠%S]) css (ValR [☠%S]) cst) → r ⊨ˢ{n,fs,ft} (Retag (Place l (Tagged tg) (Reference (RefPtr Mutable) ty)) Default, css) ≥ ... ... @@ -337,15 +336,18 @@ Proof. intros [Hrel1 ?]%rrel_with_eq [Hrel2 ?]%rrel_with_eq. simplify_eq. Admitted. Lemma sim_simple_copy_shared fs ft r n (rs rt: result) css cst Φ : rrel r rs rt → (∀ r' (v1 v2: result), rrel r' v1 v2 → (∀ r' (v1 v2: value), (* this post-condition is weak, we can return related values *) vrel r' v1 v2 → Φ (r ⋅ r') n v1 css v2 cst) → r ⊨ˢ{n,fs,ft} (Copy rs, css) ≥ (Copy rt, cst) : Φ. Proof. intros [Hrel ?]%rrel_with_eq. simplify_eq. Admitted. intros [Hrel <-]%rrel_with_eq HH σs σt <-<-. eapply sim_body_copy_public; eauto. Qed. Lemma sim_simple_retag_shared fs ft r n (rs rt: result) k css cst Φ : rrel r rs rt → ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!