Commit 482e479b authored by Hai Dang's avatar Hai Dang

complete ex3_1

parent 0cc1b8ee
From stbor.sim Require Import local invariant refl.
From stbor.sim Require Import tactics simple program.
From stbor.sim Require Import refl_step right_step left_step derived_step.
From stbor.sim Require Import refl_step right_step left_step derived_step viewshift.
Set Default Proof Using "Type".
......@@ -40,7 +40,7 @@ Definition ex3_opt_2 : function :=
.
(* TODO: show refinement to be transitive *)
Lemma ex3_sim_fun : ⊨ᶠ ex3_unopt ex3_opt_1.
Lemma ex3_1_sim_fun : ⊨ᶠ ex3_unopt ex3_opt_1.
Proof.
(* We can't use sim_simple because we need to track our stack frame id *)
intros fs ft LOOK rarg es et vls vlt σs σt FREL SUBSTs SUBSTt.
......@@ -85,7 +85,8 @@ Proof.
(* Copy local place *)
sim_apply sim_body_copy_local; [solve_sim..|].
sim_apply sim_body_result => /= VALID.
sim_apply (sim_body_deref _ _ _ _ (ValR _)).
sim_bind (Deref _ _) (Deref _ _). (* TODO: sim_apply fails to instantiate evars *)
apply (sim_body_deref _ _ _ _ (ValR _)).
move => ?? Eq. symmetry in Eq. simplify_eq/=.
(* Write unique of 42 *)
sim_apply sim_body_write_unique_1;
......@@ -97,10 +98,10 @@ Proof.
apply: sim_body_result=>_/=.
(* Write protected right *)
sim_apply_r sim_body_deref_r =>/=.
sim_apply_r sim_body_write_protected_r;
[solve_sim..|by rewrite lookup_insert |by rewrite lookup_insert
sim_apply_r sim_body_write_non_ptr_protected_r;
[solve_sim..|by rewrite lookup_insert|by rewrite lookup_insert
|by eapply (elem_of_dom_2 _ _ _ Eql')|].
intros Eqss3 σt3' rt'. simpl.
move => Eqss3 σt3' rt'.
apply: sim_body_result=>_/=.
sim_apply sim_body_let_r =>/=.
(* Call *)
......@@ -116,4 +117,55 @@ Proof.
apply: sim_body_result=>_/=.
(* Write protected left *)
sim_apply_l sim_body_deref_l =>/=.
Abort.
subst rt'. rewrite insert_insert.
sim_apply_l sim_body_write_non_ptr_protected_l;
[solve_sim..|by rewrite lookup_insert|by rewrite lookup_insert
|by eapply (elem_of_dom_2 _ _ _ Eql')|].
move => Eqst4 σt4' rt'.
apply: sim_body_result=>_ /=.
sim_apply sim_body_let_l =>/=.
(* Free stuff *)
sim_apply sim_body_free_unique_local_1;
[done|rewrite /res_loc /= insert_empty; solve_sim |by left|].
move => _ _ α5 _ σs5 σt5.
sim_apply sim_body_let=>/=.
(* Remove protection *)
set r1 := rarg res_cs σt.(snc) {[tnew := dom (gset loc) hplt]} r0 rf' rt'.
set r2 := rarg res_cs σt.(snc) r0 rf' rt'.
apply (viewshift_state_sim_local_body _ _ _ _ r1 r2).
{ rewrite /r1 /r2. do 3 apply viewshift_state_frame_r.
apply vs_state_drop_protector; [done|].
move => l1 /InD [i [/= Lti ?]]. subst l1.
destruct i; [|clear -Lti; by lia]. rewrite shift_loc_0_nat.
move => ss5 /= /lookup_delete_Some [? Eqst5].
rewrite Eqst5 in Eqst4. simplify_eq. exists (ScInt 13).
rewrite lookup_delete_ne; [|done].
by rewrite lookup_insert. }
(* Finishing up. *)
apply: sim_body_result => Hval. split.
- exists σt.(snc). split; [done|]. rewrite /end_call_sat.
apply (cmap_lookup_op_unique_included (res_cs σt.(snc) ).(rcm));
[apply Hval|apply prod_included; rewrite /r2; solve_res|..].
by rewrite res_cs_lookup.
- move : VREL'. rewrite /r2. apply vrel_mono; [done|solve_res].
Qed.
(** Top-level theorem: Two programs that only differ in the
"ex3" function are related. *)
Corollary ex3_1 (prog: fn_env) :
stuck_decidable
prog_wf prog
let prog_src := <["ex3":=ex3_unopt]> prog in
let prog_tgt := <["ex3":=ex3_opt_1]> 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: ex3_1_sim_fun.
- exact: sim_mod_funs_refl.
Qed.
Print Assumptions ex3_1.
......@@ -253,4 +253,190 @@ Proof.
+ econstructor 2; eauto. by etrans.
Qed.
(* Protected write *)
Lemma sim_body_write_non_ptr_protected_l
fs ft (r r' r'': resUR) (h: heaplet) n (l: loc) t T (ss st ss': scalar)
c Ts L et σs σt Φ :
(if ss' is ScPtr l' t' then False else True)
let tk := tkUnique in
tsize T = 1%nat
r r' res_tag t tk h
r' r'' res_cs c Ts
h !! l = Some (ss, st)
Ts !! t = Some L
l L
(σt.(shp) !! l = Some st
let σs' := mkState (<[l := ss']> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
let rt' := res_tag t tk (<[l := (ss', st)]> h) in
r' rt' {n,fs,ft} (#[], σs') (et, σt) : Φ : Prop)
r {n,fs,ft} (Place l (Tagged t) T <- #[ss'], σs) (et, σt) : Φ.
Proof.
intros NL tk LenT Eqr Eqr' Eqs EqTs InL CONT. pfold.
intros NT r_f WSAT. have WSAT1 := WSAT.
destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
have HLc: (r_f r).(rcm) !! c Excl' Ts.
{ rewrite Eqr Eqr' 2!cmra_assoc lookup_op right_id.
apply (cmap_lookup_op_unique_included (res_cs c Ts).(rcm)).
- move : (proj2 VALID). rewrite Eqr Eqr' 2!cmra_assoc => VALID2.
by apply (cmra_valid_included _ _ VALID2), cmra_included_l.
- by apply cmra_included_r.
- by rewrite res_cs_lookup. }
destruct (CINV _ _ HLc) as [INc CINVc].
specialize (CINVc _ _ EqTs) as [Ltc CINVc].
specialize (CINVc _ InL) as (stk & pm & Eqstk & Instk & NDIS).
have HLtrf : (r_f r).(rtm) !! t Some (to_tgkR tk, to_agree <$> h).
{ rewrite ->Eqr in VALID. move : VALID. rewrite cmra_assoc => VALID.
rewrite Eqr cmra_assoc.
apply tmap_lookup_op_r_uniq_equiv; [apply VALID|].
by rewrite res_tag_lookup. }
have HLl : (to_agree <$> h) !! l Some (to_agree (ss, st))
by rewrite lookup_fmap Eqs.
destruct (PINV _ _ _ HLtrf) as [Ltt Pt].
specialize (Pt l ss st HLl) as (Eqst & Eqss & TPO).
{ by exists stk, pm, (Some c). }
have [ns Eqstk']: n, access1 stk AccessWrite (Tagged t) σs.(scs) = Some (n, stk).
{ destruct TPO as (stk1 & Eqstk1 & pro & TPO).
rewrite Eqstk1 in Eqstk. simplify_eq.
by eapply tag_unique_head_access. }
have Eqα : memory_written σs.(sst) σs.(scs) l (Tagged t) (tsize T) = Some σs.(sst).
{ destruct SREL as (EQss & _).
rewrite LenT /memory_written /= shift_loc_0_nat EQss
Eqstk /= Eqstk' /= insert_id //. }
set σs' := mkState (<[l := ss']> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc).
have STEPS: ((Place l (Tagged t) T <- #[ss'])%E, σs) ~{fs}~> (#[]%E, σs').
{ eapply (head_step_fill_tstep _ []); eapply write_head_step'; eauto.
- move => ?? /elem_of_list_singleton ?. by subst ss'.
- clear -Eqss LenT.
intros i. rewrite LenT=>?. destruct i; [|lia].
rewrite shift_loc_0_nat. by eapply elem_of_dom_2. }
have STEPSS: ((Place l (Tagged t) T <- #[ss'])%E, σs) ~{fs}~>* (#[]%E, σs')
by apply rtc_once.
set rt' := res_tag t tk (<[l := (ss', st)]> h).
have EQrcm: (r_f r).(rcm) (r_f r' rt').(rcm)
by rewrite Eqr cmra_assoc.
have HLNt: (r_f r').(rtm) !! t = None.
{ destruct ((r_f r').(rtm) !! t) as [ls|] eqn:Eqls; [|done].
exfalso. move : HLtrf.
rewrite Eqr cmra_assoc lookup_op Eqls res_tag_lookup.
apply tagKindR_exclusive_heaplet. }
have HLtrf' :
(r_f r' rt').(rtm) !! t Some (to_tgkR tk, to_hplR (<[l:=(ss', st)]> h)).
{ by rewrite lookup_op HLNt res_tag_lookup left_id. }
have VALIDr: (r_f r' rt').
{ move : VALID. rewrite Eqr cmra_assoc => VALID.
apply (local_update_discrete_valid_frame _ _ _ VALID).
apply res_tag_uniq_local_update; [by right|done]. }
have WSAT': wsat (r_f (r' rt')) σs' σt.
{ rewrite cmra_assoc.
split; last split; last split; last split; last split.
- by apply (tstep_wf _ _ _ STEPS WFS).
- done.
- done.
- intros t1 k1 h1 Eqh1.
case (decide (t1 = t)) => ?; [subst t1|].
+ split; [done|].
specialize (PINV _ _ _ HLtrf) as [? PINV].
have [? Eqh]: k1 = tk h1 to_agree <$> (<[l:=(ss', st)]> h).
{ move : Eqh1. rewrite HLtrf'.
by intros [?%leibniz_equiv_iff%to_tgkR_inj ?]%Some_equiv_inj. } subst k1.
intros l1 ss1 st1. rewrite Eqh lookup_fmap.
case (decide (l1 = l)) => ?; [subst l1|].
* rewrite lookup_insert. intros Eq%Some_equiv_inj%to_agree_inj.
symmetry in Eq. simplify_eq.
rewrite /= lookup_insert. intros PRE. do 2 (split; [done|]).
specialize (PINV l ss st). rewrite lookup_fmap Eqs in PINV.
by specialize (PINV ltac:(done) PRE) as (Eqst1 & Eqss1 & HD).
* rewrite lookup_insert_ne // -lookup_fmap.
intros Eq. specialize (PINV _ _ _ Eq).
by rewrite /σs' lookup_insert_ne.
+ have Eqh : (r_f r).(rtm) !! t1 Some (to_tgkR k1, h1).
{ rewrite Eqr cmra_assoc lookup_op res_tag_lookup_ne; [|done].
move : Eqh1. by rewrite lookup_op res_tag_lookup_ne. }
specialize (PINV _ _ _ Eqh) as [Ltt1 PINV].
split; [done|]. intros l1 ss1 st1 Eql1 PRE.
specialize (PINV _ _ _ Eql1 PRE) as (Eqst1 & Eqss1 & HPO).
rewrite /= lookup_insert_ne; [done|].
intros ?. subst l1.
(* t1 t, t is top of stack(l), t1 is top or SRO in stack (l).
This cannot happen. *)
exfalso.
have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
destruct k1; simpl in *.
{ rewrite Eqstk in HPO. simplify_eq.
eapply (access1_write_remove_incompatible_head _ (Tagged t) t1 _ _ _ ND);
eauto.
- by exists None, [].
- by inversion 1.
- by left. }
{ destruct HPO as (stk1 & Eqstk1 & opro & HD).
rewrite Eqstk1 in Eqstk. simplify_eq.
eapply (access1_write_remove_incompatible_head _ (Tagged t) t1 _ _ _ ND);
eauto.
- by inversion 1.
- destruct HD as [? HD]. rewrite HD. by left. }
{ destruct HPO as (stk1 & Eqstk1 & HD).
rewrite Eqstk1 in Eqstk. simplify_eq.
destruct PRE as (stk1 & pm1 & opro & Eqstk & In1 & ?).
rewrite Eqstk in Eqstk1. simplify_eq.
eapply (access1_write_remove_incompatible_active_SRO _
(Tagged t) t1 _ _ _ ND); eauto. }
- move => ??. rewrite -EQrcm. by apply CINV.
- destruct SREL as (?&?&?&?& PB). do 4 (split; [done|]).
move => l1 /= InD.
case (decide (l1 = l)) => ?; [subst l1|].
{ right.
exists t, tk, (to_hplR (<[l := (ss', st)]> h)). split; last split.
- done.
- rewrite /to_hplR lookup_fmap lookup_insert. by eexists.
- right. split; [done|]. exists c, Ts, L.
rewrite -EQrcm. by rewrite HLc. }
specialize (PB _ InD) as [PB|[t1 PV]]; [left|right].
{ intros st1. rewrite /= lookup_insert_ne; [|done].
move => /PB [ss1 [Eqss1 ARELs]].
exists ss1. split; [done|].
move : ARELs. rewrite Eqr cmra_assoc.
apply arel_res_tag_overwrite. by right. }
destruct PV as (k1 & h1 & Eqt1 & IS1 & CASE).
case (decide (t1 = t)) => ?; [subst t1|].
{ have [? Eqh]: k1 = tk h1 to_agree <$> h.
{ move : Eqt1. rewrite HLtrf.
by intros [?%leibniz_equiv_iff%to_tgkR_inj ?]%Some_equiv_inj. }
subst k1.
exists t, tk, (to_hplR (<[l := (ss', st)]> h)). split; last split.
- done.
- rewrite /to_hplR lookup_fmap lookup_insert_ne; [|done].
move : (Eqh l1). destruct IS1 as [? Eq1].
rewrite Eq1 lookup_fmap.
destruct (h !! l1) eqn:Eqhl1; rewrite Eqhl1;
[by eexists|by inversion 1].
- by setoid_rewrite <- EQrcm. }
exists t1, k1, h1. setoid_rewrite <- EQrcm. split; [|done].
rewrite lookup_op res_tag_lookup_ne; [|done].
move : Eqt1. by rewrite Eqr cmra_assoc lookup_op res_tag_lookup_ne. }
have NT' := never_stuck_tstep_once _ _ _ _ _ STEPS NT.
specialize (CONT Eqst). punfold CONT.
specialize (CONT NT' _ WSAT') as [RE TE ST]. split; [done|..].
- intros. specialize (TE _ TERM) as (vs' & σs1 & r1 & STEPS' & POST).
exists vs', σs1, r1. split; [|done]. etrans; eauto.
- inversion ST.
+ constructor 1. intros.
destruct (STEP _ _ STEPT) as (es' & σs1 & r1 & n' & STEPS' & POST).
exists es', σs1, 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.
......@@ -304,7 +304,7 @@ Qed.
(* Protected write *)
Lemma sim_body_write_protected_r
Lemma sim_body_write_non_ptr_protected_r
fs ft (r r' r'': resUR) (h: heaplet) n (l: loc) t T (ss st st': scalar)
c Ts L es σs σt Φ :
(if st' is ScPtr l' t' then False else True)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment