Commit 237f63fc authored by Hai Dang's avatar Hai Dang

complete ex2

parent 4aba43b3
......@@ -37,6 +37,7 @@ theories/sim/refl_mem_step.v
theories/sim/refl_step.v
theories/sim/left_step.v
theories/sim/right_step.v
theories/sim/derived_step.v
theories/sim/simple.v
theories/sim/refl.v
......
......@@ -51,7 +51,7 @@ Proof.
apply sim_simple_valid_post.
apply: sim_simple_result. simpl. intros VALID.
(* Retag *)
sim_apply sim_simple_retag_mut_ref; [simpl; lia| |eauto|..].
sim_apply sim_simple_retag_ref; [simpl; lia|done| |eauto|..].
{ eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
move=>l_i tg_i tg_n hplt /= ? IS_i. subst sarg.
specialize (IS_i O ltac:(lia)). rewrite shift_loc_0_nat in IS_i.
......
From stbor.sim Require Import local invariant refl_step.
From stbor.sim Require Import tactics simple program.
From stbor.sim Require Import refl_step right_step left_step viewshift.
Set Default Proof Using "Type".
......@@ -24,7 +26,90 @@ Definition ex1_down_opt : function :=
Copy *{int} "x"
.
Lemma ex1_down_sim_fun : ⊨ᶠ ex1_down ex1_down_opt.
Proof.
apply (sim_fun_simple1 10)=>// fs ft rarg es et arg c LOOK AREL ??.
simplify_eq/=.
(* Alloc local *)
sim_apply sim_simple_alloc_local=> l t /=.
sim_apply sim_simple_let=>/=.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros sarg ->.
sim_apply sim_simple_let=>/=.
apply: sim_simple_result.
(* Retag a local place *)
sim_apply sim_simple_let=>/=.
apply Forall2_cons_inv in AREL as [AREL _].
sim_apply sim_simple_let=>/=.
(* Copy local place *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply sim_simple_valid_post.
apply: sim_simple_result. simpl. intros VALID.
(* TODO: need a rule to add a tag to res_cs.
Also need a rule to remove it at the end. *)
(* Retag *)
(* sim_apply sim_simple_retag_mut_ref; [simpl; lia| |eauto|..].
{ eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
move=>l_i tg_i tg_n hplt /= ? IS_i. subst sarg.
specialize (IS_i O ltac:(lia)). rewrite shift_loc_0_nat in IS_i.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros s ?. simplify_eq.
(* Call *)
sim_apply sim_simple_let=>/=.
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=.
(* Copy local *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply: sim_simple_result. simpl.
sim_apply sim_simple_deref=>l' t' ?. simplify_eq/=.
(* Write unique. We need to drop to complex mode, to preserve some local state info. *)
intros σs σt.
sim_apply sim_body_write_unique_1; [solve_sim..|].
intros ?? Htop. simplify_eq/=.
sim_apply sim_body_let. simplify_eq/=.
(* Copy local (right) *)
sim_apply_r sim_body_copy_local_r; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy unique (right) *)
sim_apply_r sim_body_deref_r. simpl.
sim_apply_r sim_body_copy_unique_r; [try solve_sim..|].
{ rewrite lookup_insert. done. }
apply: sim_body_result=>_. simpl.
apply: sim_body_let_r. simpl. (* FIXME: figure out why [sim_apply_r] does the wrong thing here *)
(* We can go back to simple mode! *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
simplify_eq/=. clear- AREL FREL LOOK.
(* Call *)
sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=.
(* Copy local (left). We drop to complex just because simple does not support this yet. *)
intros σs σt.
sim_apply_l sim_body_copy_local_l; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy unique (left) *)
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
{ rewrite lookup_insert. done. }
apply: sim_body_result=>Hval. simpl.
apply: sim_body_let_l. simpl.
(* Free stuff *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
sim_apply sim_simple_free_local_1; [solve_sim..|]. simpl.
sim_apply sim_simple_let=>/=.
sim_apply sim_simple_free_public.
{ simpl. constructor; [|by constructor].
apply: arel_mono; last fast_done.
apply: cmra_valid_included; first fast_done.
do 3 apply cmra_mono_r. solve_res. solve_res. }
sim_apply sim_simple_let=>/=.
(* Finishing up. *)
apply: sim_simple_result. split.
- solve_res.
- constructor; simpl; auto. *)
Abort.
From stbor.sim Require Import local invariant refl_step.
From stbor.sim Require Import local invariant refl tactics simple program
refl_step right_step left_step viewshift derived_step.
Set Default Proof Using "Type".
(** Moving read of shared ref up across code that *may* use that ref. *)
(* Assuming x : & i32 *)
Definition ex2 : function :=
Definition ex2_unopt : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
retag_place "x" (RefPtr Immutable) int Default ;;
Copy *{int} "x" ;;
Call #[ScFnPtr "f"] ["x"] ;;
Call #[ScFnPtr "f"] [Copy "x"] ;;
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
"v"
......@@ -20,13 +20,118 @@ Definition ex2_opt : function :=
fun: ["i"],
let: "x" := new_place (& int) "i" in
retag_place "x" (RefPtr Immutable) int Default ;;
Copy *{int} "x" ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] ["x"] ;;
Call #[ScFnPtr "f"] [Copy "x"] ;;
Free "x" ;; Free "i" ;;
"v"
.
Lemma ex2_sim_body : ⊨ᶠ ex2 ex2_opt.
Lemma ex2_sim_body : ⊨ᶠ ex2_unopt ex2_opt.
Proof.
Abort.
apply (sim_fun_simple1 10)=>// fs ft rarg es et arg c LOOK AREL ??.
simplify_eq/=.
(* Alloc local *)
sim_apply sim_simple_alloc_local=> l t /=.
sim_apply sim_simple_let=>/=.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros sarg ->.
sim_apply sim_simple_let=>/=.
apply: sim_simple_result.
(* Retag a local place *)
sim_apply sim_simple_let=>/=.
apply Forall2_cons_inv in AREL as [AREL _].
(* We need to drop to complex mode, to preserve some local state info. *)
intros σs σt.
sim_apply sim_body_let=>/=.
(* Copy local place *)
sim_apply sim_body_copy_local; [solve_sim..|].
sim_apply sim_body_result. simpl. intros VALID.
(* Retag *)
sim_apply sim_body_retag_ref_default; [simpl; lia|done| |eauto|..].
{ eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
move=> l' told tnew hplt c' cids α' nxtp' ? _ _ IS_i σs' σt' s_new
tk ARELn /=. subst sarg.
specialize (IS_i O ltac:(simpl; lia)). rewrite shift_loc_0_nat in IS_i.
destruct IS_i as [[[ss st] IS_i] TOP].
(* Write local *)
sim_apply sim_body_write_local_1; [solve_sim..|].
intros s ?. simplify_eq. simpl.
sim_apply sim_body_let. simplify_eq/=.
(* Copy local (right) *)
sim_apply_r sim_body_copy_local_r; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy public right *)
sim_apply_r sim_body_deref_r. simpl.
sim_apply_r sim_body_copy_SRO_public_r; [solve_sim..|].
apply: sim_body_result=>_. simpl.
apply: sim_body_let_r. simpl.
(* Back to simple mode! *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
simplify_eq/=.
(* Copy local *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply: sim_simple_result. simpl.
(* Call *)
rewrite (_: rarg res_cs c res_tag tnew tk hplt
res_loc l [(ScPtr l' (Tagged tnew), ScPtr l' (Tagged tnew))] t
rarg res_cs c res_tag tnew tk hplt
res_loc l [(ScPtr l' (Tagged tnew), ScPtr l' (Tagged tnew))] t
res_tag tnew tk hplt); last first.
{ rewrite {1}res_tag_public_dup cmra_assoc. solve_res. }
sim_apply (sim_simple_call 5 [ValR [ScPtr l' (Tagged tnew)]]
[ValR [ScPtr l' (Tagged tnew)]]
(res_tag tnew tkPub hplt)); [solve_sim..| |].
{ constructor; [|by constructor].
constructor; [done|by constructor]. } clear ARELn.
intros rf' frs' frt' ??? ? _ _ FREL'. simplify_eq/=.
apply: sim_simple_result. simpl.
sim_apply sim_simple_let=>/=. clear σs' σt' nxtp' α' TOP σs σt.
(* Copy local (left). We drop to complex just because simple does not support this yet. *)
intros σs σt.
sim_apply_l sim_body_copy_local_l; [solve_sim..|].
apply: sim_body_result=>_. simpl.
(* Copy public (left) *)
sim_apply_l sim_body_deref_l. simpl.
sim_apply_l sim_body_copy_public_l; [try solve_sim..|].
intros r' AREL'.
apply: sim_body_result=>Hval. simpl.
apply: sim_body_let_l. simpl.
(* Free stuff *)
eapply (sim_simplify (fun_post_simple c)). { by eauto. }
sim_apply sim_simple_free_local_1; [solve_sim..|]. simpl.
sim_apply sim_simple_let=>/=.
sim_apply sim_simple_free_public.
{ simpl. constructor; [|by constructor].
apply: arel_mono; last fast_done.
apply: cmra_valid_included; first fast_done.
do 2 apply cmra_mono_r. solve_res. solve_res. }
sim_apply sim_simple_let=>/=.
(* Finishing up. *)
apply: sim_simple_result. split.
- solve_res.
- constructor; simpl; auto.
eapply arel_mono; [..|solve_res|exact AREL'].
eapply cmra_valid_included; [exact Hval|].
do 2 apply cmra_mono_r. solve_res.
Qed.
(** Top-level theorem: Two programs that only differ in the
"ex2" function are related. *)
Corollary ex2 (prog: fn_env) :
stuck_decidable
prog_wf prog
let prog_src := <["ex2":=ex2_unopt]> prog in
let prog_tgt := <["ex2":=ex2_opt]> prog in
behave_prog prog_tgt <1= behave_prog prog_src.
Proof.
intros Hdec Hwf. apply sim_prog_sim_classical.
{ apply Hdec. }
{ apply has_main_insert, Hwf; done. }
apply sim_mod_funs_local.
apply sim_mod_funs_insert; first done.
- exact: ex2_sim_body.
- exact: sim_mod_funs_refl.
Qed.
Print Assumptions ex2.
From stbor.sim Require Import local invariant refl_step.
From stbor.sim Require Import tactics simple program.
From stbor.sim Require Import refl_step right_step left_step viewshift.
Set Default Proof Using "Type".
......@@ -28,4 +30,22 @@ Definition ex2_down_opt : function :=
Lemma ex2_down_sim_fun : ⊨ᶠ ex2_down ex2_down_opt.
Proof.
apply (sim_fun_simple1 10)=>// fs ft rarg es et arg c LOOK AREL ??.
simplify_eq/=.
(* Alloc local *)
sim_apply sim_simple_alloc_local=> l t /=.
sim_apply sim_simple_let=>/=.
(* Write local *)
sim_apply sim_simple_write_local; [solve_sim..|].
intros sarg ->.
sim_apply sim_simple_let=>/=.
apply: sim_simple_result.
(* Retag a local place *)
sim_apply sim_simple_let=>/=.
apply Forall2_cons_inv in AREL as [AREL _].
sim_apply sim_simple_let=>/=.
(* Copy local place *)
sim_apply sim_simple_copy_local; [solve_sim..|].
apply sim_simple_valid_post.
apply: sim_simple_result. simpl. intros VALID.
Abort.
......@@ -587,3 +587,14 @@ Proof.
by apply op_local_update_frame, res_tag_uniq_dealloc_local_update.
Qed.
Lemma res_tag_public_dup t hplt:
res_tag t tkPub hplt res_tag t tkPub hplt res_tag t tkPub hplt.
Proof.
split.
- intros t'. rewrite lookup_op. case (decide (t' = t)) => ?.
+ subst t'. rewrite res_tag_lookup.
rewrite -Some_op -pair_op.
rewrite -{2}(heaplet_core (to_agree <$> hplt)) cmra_core_l //.
+ rewrite res_tag_lookup_ne // right_id //.
- rewrite /= right_id //.
Qed.
From stbor.sim Require Import left_step right_step.
Lemma sim_body_copy_local fs ft r r' n l t ty ss st σs σt Φ :
tsize ty = 1%nat
r r' res_loc l [(ss, st)] t
(r {n,fs,ft} (#[ss], σs) (#[st], σt) : Φ)
r {S n,fs,ft}
(Copy (Place l (Tagged t) ty), σs) (Copy (Place l (Tagged t) ty), σt)
: Φ.
Proof.
intros ?? Hcont.
eapply sim_body_copy_local_l; [done..|].
eapply sim_body_copy_local_r; done.
Qed.
......@@ -163,3 +163,43 @@ Proof.
by inversion Eq. } subst opro.
by eexists.
Qed.
Lemma public_read_head r σs (σt: state) l stk n' stk' t ss st h:
σt.(sst) !! l = Some stk
access1 stk AccessRead (Tagged t) σt.(scs) = Some (n', stk')
wsat r σs σt
r.(rtm) !! t Some (to_tgkR tkPub, h)
h !! l Some $ to_agree (ss,st)
it, it stk it.(tg) = Tagged t it.(perm) Disabled
t active_SRO stk
σt.(shp) !! l = Some st σs.(shp) !! l = Some ss arel r ss st.
Proof.
intros Eqstk ACC WSAT HL Eqs.
have WSAT1 := WSAT.
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc & PV).
specialize (PINV _ _ _ HL) as [? PINV].
specialize (PINV _ _ _ Eqs).
destruct (access1_in_stack _ _ _ _ _ _ ACC) as (it & Init & Eqti & NDIS).
destruct PINV as [Eqss [Eqss' HD]].
{ rewrite /= -Eqti. exists stk, it.(perm), it.(protector).
repeat split; [done| |done]. by destruct it. }
destruct HD as (stk1 & Eqstk1 & InSRO).
rewrite Eqstk1 in Eqstk. simplify_eq.
exists it. repeat split; [done..|].
destruct (PV l) as [PB|[t' PR]]; cycle 2.
{ exfalso.
have Eq :=
priv_loc_UB_access_eq _ _ AccessRead σs σt t' (Tagged t) _ Eqstk1
ltac:(by eexists) WSAT1 PR.
simplify_eq.
destruct PR as (k1 & h1 & Eqh1 & ? & CASE).
move : Eqh1. rewrite HL.
rewrite -(left_id None op (Some _)).
destruct CASE as [|[]]; subst k1.
- apply tagKindR_local_exclusive_r.
- apply tagKindR_uniq_exclusive_r. }
{ rewrite (state_wf_dom _ WFT) elem_of_dom. by eexists. }
destruct (PB _ Eqss) as (st' & Eqst' & AREL). rewrite Eqst' in Eqss'.
by simplify_eq.
Qed.
......@@ -52,6 +52,7 @@ Proof.
move : STEPT. rewrite <-into_result. by rewrite to_of_result.
Qed.
(* Unique/Local copy *)
Lemma sim_body_copy_local_unique_l
fs ft (r r': resUR) (h: heaplet) n (l: loc) t k T (ss st: scalar) et σs σt Φ
(LU: k = tkLocal k = tkUnique) :
......@@ -171,4 +172,85 @@ Proof.
by rewrite lookup_insert.
Qed.
(* Public SRO copy *)
Lemma sim_body_copy_public_l
fs ft (r r': resUR) (h: heaplet) n (l: loc) t T (ss st: scalar) et σs σt Φ :
tsize T = 1%nat
r r' res_tag t tkPub h
h !! l = Some (ss,st)
( r', arel r' ss st r r' {n,fs,ft} (#[ss], σs) (et, σt) : Φ : Prop)
r {n,fs,ft} (Copy (Place l (Tagged t) T), σs) (et, σt) : Φ.
Proof.
intros LenT Eqr Eqs CONT. pfold. intros NT. intros.
have WSAT1 := WSAT. (* backup *)
(* making a step *)
edestruct (NT (Copy (Place l (Tagged t) T)) σs) as [[]|[es' [σs' STEPS]]];
[done..|].
destruct (tstep_copy_inv _ (PlaceR _ _ _) _ _ _ STEPS)
as (l'&t'&T'& vs & α' & EqH & ? & Eqvs & Eqα' & ?).
symmetry in EqH. simplify_eq.
rewrite LenT read_mem_equation_1 /= in Eqvs.
destruct (σs.(shp) !! l) as [s'|] eqn:Eqs'; [|done].
simpl in Eqvs. simplify_eq.
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
(* some lookup properties *)
have [h' HLtrf]: h', (r_f r).(rtm) !! t
Some (to_tgkR tkPub, h' (to_agree <$> h)).
{ setoid_rewrite Eqr. setoid_rewrite cmra_assoc.
apply tmap_lookup_op_r_equiv_pub.
- move : VALID. rewrite Eqr cmra_assoc => VALID. apply VALID.
- rewrite res_tag_lookup //. }
have HLl : (h' (to_agree <$> h)) !! l Some (to_agree (ss, st)).
{ move : (proj1 VALID t). rewrite HLtrf. move => [_ /= /(_ l)].
rewrite lookup_op lookup_fmap Eqs /=.
destruct (h' !! l) as [sst|] eqn:Eql; rewrite Eql; [|by rewrite left_id].
rewrite -Some_op => /agree_op_inv ->. by rewrite agree_idemp. }
(* Public: stack unchanged *)
destruct (for_each_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
specialize (EQ1 O) as (stk & stk' & Eqstk & Eqstk' & ACC1); [rewrite LenT; lia|].
rewrite shift_loc_0_nat in Eqstk, Eqstk'.
move : ACC1. case access1 as [[n1 stk1]|] eqn:ACC1; [|done].
simpl. intros Eqs1. symmetry in Eqs1. simplify_eq.
destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
rewrite Eqst in Eqstk. rewrite Eqcs in ACC1.
destruct (public_read_head _ _ _ _ _ _ _ _ _ _ _ Eqstk ACC1 WSAT1 HLtrf HLl)
as (it & Init & Eqti & NDIS & HDi & Eqhpt & Eqhps & AREL').
apply arel_persistent in AREL'.
rewrite Eqs' in Eqhps. simplify_eq.
have ?: α' = σt.(sst).
{ move : Eqα'.
rewrite LenT /= /memory_read /= /= shift_loc_0_nat Eqst Eqstk /= Eqcs ACC1 /=.
destruct (tag_SRO_top_access σt.(scs) stk t HDi) as [ns Eqss].
rewrite ACC1 in Eqss. simplify_eq. rewrite insert_id //. by inversion 1. }
subst α'. rewrite Eqstk in Eqstk'. symmetry in Eqstk'. simplify_eq.
rewrite (_: mkState σs.(shp) σt.(sst) σs.(scs) σs.(snp) σs.(snc) = σs) in STEPS;
last first. { rewrite -Eqst. by destruct σs. }
have STEPSS: (Copy (Place l (Tagged t) T), σs) ~{fs}~>* (#[ss]%E, σs)
by apply rtc_once.
have NT' := never_stuck_tstep_once _ _ _ _ _ STEPS NT.
(* TODO: the following is the same in most proofs, generalize it *)
specialize (CONT _ AREL').
punfold CONT.
move : WSAT1. rewrite -(cmra_core_r (r_f r)) -cmra_assoc. intros WSAT.
specialize (CONT NT' _ WSAT) as [RE TE ST]. split; [done|..].
- intros. specialize (TE _ TERM) as (vs' & σs' & r1 & STEPS' & POST).
exists vs', σs', r1. split; [|done]. etrans; eauto.
- inversion ST.
+ constructor 1. intros.
destruct (STEP _ _ STEPT) as (es' & σs' & r1 & n' & STEPS' & POST).
exists es', σs', r1, n'. split; [|done].
left. destruct STEPS' as [?|[]].
* eapply tc_rtc_l; eauto.
* simplify_eq. by apply tc_once.
+ econstructor 2; eauto. by etrans.
Qed.
End left.
......@@ -1407,7 +1407,6 @@ Proof.
- by apply IH.
Qed.
Lemma sim_body_retag_ref_default fs ft mut r n ptr T σs σt Φ :
(0 < tsize T)%nat
let pk : pointer_kind := (RefPtr mut) in
......@@ -1429,6 +1428,7 @@ Lemma sim_body_retag_ref_default fs ft mut r n ptr T σs σt Φ :
let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in
let s_new := ScPtr l (Tagged tnew) in
let tk := match mut with Mutable => tkUnique | Immutable => tkPub end in
(if mut is Immutable then arel (res_tag tnew tk hplt) s_new s_new else True)
Φ (r res_tag tnew tk hplt) n (ValR [s_new]) σs' (ValR [s_new]) σt')
r {n,fs,ft}
(Retag #[ptr] pk T Default, σs)
......@@ -1505,13 +1505,12 @@ Proof.
exists (#[ScPtr l (Tagged tnew)])%V, σs', r', n.
split; last split.
{ left. by constructor. }
{ clear POST.
{ clear POST. rewrite /r' cmra_assoc.
split; last split; last split; last split; last split.
- by apply (tstep_wf _ _ _ STEPS WFS).
- by apply (tstep_wf _ _ _ STEPT WFT).
- by rewrite cmra_assoc.
- clear STEPS STEPT.
rewrite cmra_assoc. intros t' k' h'. rewrite lookup_op.
- done.
- clear STEPS STEPT. intros t' k' h'. rewrite lookup_op.
case (decide (t' = tnew)) => ?; [subst t'|].
+ rewrite res_tag_lookup HNP left_id.
intros [Eq1%leibniz_equiv_iff Eq2]%Some_equiv_inj.
......@@ -1603,7 +1602,7 @@ Proof.
by apply (retag_item_active_SRO_preserving _ _ _ _ _ _ _ _ _ _ _ _ EqRT
_ _ _ _ _ ND2 Eqstk1 Eqstk' In In').
- (* TODO: duplicate proof with retag_public *)
intros c1 Tc. rewrite cmra_assoc Eqc'. intros Eqc.
intros c1 Tc. rewrite Eqc'. intros Eqc.
specialize (CINV _ _ Eqc) as [Ltc CINV].
split; [done|].
intros tc L EqL. specialize (CINV _ _ EqL) as [Ltp CINV].
......@@ -1614,22 +1613,23 @@ Proof.
_ _ _ _ _ Eqstk Ltc In) as (stk' & Eqstk' & In').
by exists stk', pm'.
- (* TODO: duplicate proof with retag_public *)
rewrite cmra_assoc. do 4 (split; [done|]).
do 4 (split; [done|]).
move => l' /PUBP [PB|PV].
+ left. move => ? /PB [? [? AREL']]. eexists. split; [done|].
+ 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.
apply: sim_body_result. intros VALIDr. eapply POST; eauto.
intros i Lti. split.
- clear -Lti EqlT.
apply write_hpl_is_Some. by rewrite EqlT.
- move : Lti.
destruct mut.
+ eapply tag_on_top_retag_ref_uniq. exact EqRT.
+ eapply tag_on_top_retag_ref_shr; [done|exact EqRT].
- intros i Lti. split.
+ clear -Lti EqlT. apply write_hpl_is_Some. by rewrite EqlT.
+ move : Lti.
destruct mut.
* eapply tag_on_top_retag_ref_uniq. exact EqRT.
* eapply tag_on_top_retag_ref_shr; [done|exact EqRT].
- destruct mut; [done|]. simpl. do 2 (split; [done|]).
rewrite lookup_insert. by eexists.
Qed.
......
......@@ -44,7 +44,7 @@ Proof.
intros. by eapply POST.
Qed.
(* Unique/Local copy *)
Lemma sim_body_copy_local_unique_r
fs ft (r r': resUR) (h: heaplet) n (l: loc) t k T (ss st: scalar) es σs σt Φ
(LU: k = tkLocal k = tkUnique) :
......@@ -60,18 +60,15 @@ Proof.
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
(* some lookup properties *)
have VALIDr := cmra_valid_op_r _ _ VALID. rewrite ->Eqr in VALIDr.
have HLtr: r.(rtm) !! t Some (to_tgkR k, to_agree <$> h).
{ rewrite Eqr. destruct LU; subst k.
- eapply tmap_lookup_op_local_included; [apply VALIDr|apply cmra_included_r|].
rewrite res_tag_lookup //.
- eapply tmap_lookup_op_uniq_included; [apply VALIDr|apply cmra_included_r|].
rewrite res_tag_lookup //. }
have HLtrf: (r_f r).(rtm) !! t Some (to_tgkR k, to_agree <$> h).
{ destruct LU; subst k.
- apply tmap_lookup_op_r_local_equiv; [apply VALID|done].
- apply tmap_lookup_op_r_uniq_equiv; [apply VALID|done]. }
{ rewrite Eqr cmra_assoc.
destruct LU; subst k.
- apply tmap_lookup_op_r_local_equiv.
+ move : VALID. rewrite Eqr cmra_assoc => VALID. apply VALID.
+ rewrite res_tag_lookup //.
- apply tmap_lookup_op_r_uniq_equiv.
+ move : VALID. rewrite Eqr cmra_assoc => VALID. apply VALID.
+ rewrite res_tag_lookup //. }
(* we can make the read in tgt because tag_on_top *)
destruct TOP as [opro TOP].
......@@ -152,4 +149,72 @@ Proof.
- by rewrite lookup_insert.
Qed.
(* Public SRO copy *)
Lemma sim_body_copy_SRO_public_r
fs ft (r r': resUR) (h: heaplet) n (l: loc) t T (ss st: scalar) es σs σt Φ :
tsize T = 1%nat
tag_on_top σt.(sst) l t SharedReadOnly
r r' res_tag t tkPub h
h !! l = Some (ss, st)
(r {n,fs,ft} (es, σs) (#[st], σt) : Φ : Prop)
r {S n,fs,ft} (es, σs) (Copy (Place l (Tagged t) T), σt) : Φ.
Proof.
intros LenT TOP Eqr Eqs CONT. pfold.
intros NT r_f WSAT. have WSAT1 := WSAT.
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
(* some lookup properties *)
have [h' HLtrf]: h', (r_f r).(rtm) !! t
Some (to_tgkR tkPub, h' (to_agree <$> h)).
{ setoid_rewrite Eqr. setoid_rewrite cmra_assoc.
apply tmap_lookup_op_r_equiv_pub.
- move : VALID. rewrite Eqr cmra_assoc => VALID. apply VALID.
- rewrite res_tag_lookup //. }
specialize (PINV _ _ _ HLtrf) as [Lt PINV].
specialize (PINV l ss st).
(* we can make the read in tgt because tag_on_top *)
have HLl : (h' (to_agree <$> h)) !! l Some (to_agree (ss, st)).
{ move : (proj1 VALID t). rewrite HLtrf. move => [_ /= /(_ l)].
rewrite lookup_op lookup_fmap Eqs /=.
destruct (h' !! l) as [sst|] eqn:Eql; rewrite Eql; [|by rewrite left_id].
rewrite -Some_op => /agree_op_inv ->. by rewrite agree_idemp. }
destruct TOP as [opro TOP].
destruct (σt.(sst) !! l) as [stk|] eqn:Eqstk; [|done]. simpl in TOP.
specialize (PINV HLl) as [Eqss [? HD]].
{ simpl.
exists stk, SharedReadOnly, opro. split; last split; [done| |done].
destruct stk; [done|]. simpl in TOP. simplify_eq. by left. }
destruct (tag_SRO_top_access σt.(scs) stk t)
as [ns Eqstk'].
{ clear -Eqstk TOP.
destruct (tag_on_top_shr_active_SRO σt.(sst) l t) as (stk1 & Eq1 & ?).
- eexists. rewrite Eqstk //.
- rewrite Eq1 in Eqstk. by simplify_eq. }
have Eqα : memory_read σt.(sst) σt.(scs) l (Tagged t) (tsize T) = Some σt.(sst).
{ rewrite LenT /memory_read /= shift_loc_0_nat Eqstk /= Eqstk' /= insert_id //. }
have READ: read_mem l (tsize T) σt.(shp) = Some [st].
{ rewrite LenT read_mem_equation_1 /= Eqss //. }
have STEPT: (Copy (Place l (Tagged t) T), σt) ~{ft}~> ((#[st])%E, σt).
{ destruct σt.
eapply (head_step_fill_tstep _ []); eapply copy_head_step'; eauto. }
split; [right; by do 2 eexists|done|].
constructor 1. intros et' σt' STEPT'.
destruct (tstep_copy_inv _ (PlaceR _ _ _) _ _ _ STEPT')
as (l1&t1&T1& vs1 & α1 & EqH & ? & Eqvs & Eqα' & ?).
symmetry in EqH. simplify_eq.
have Eqσt: mkState σt.(shp) σt.(sst) σt.(scs) σt.(snp) σt.(snc) = σt