Commit 64b1577f authored by Hai Dang's avatar Hai Dang

complete ex1_down

parent 53670eed
......@@ -29,7 +29,7 @@ Definition ex1_opt : function :=
"v"
.
Lemma ex1_sim_body :
Lemma ex1_sim_fun :
⊨ᶠ ex1_unopt ex1_opt.
Proof.
apply (sim_fun_simple1 10)=>// fs ft rarg es et arg c LOOK AREL ??.
......@@ -124,7 +124,7 @@ Proof.
{ apply has_main_insert, Hwf; done. }
apply sim_mod_funs_local.
apply sim_mod_funs_insert; first done.
- exact: ex1_sim_body.
- exact: ex1_sim_fun.
- exact: sim_mod_funs_refl.
Qed.
......
From stbor.sim Require Import local invariant refl_step.
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 viewshift.
......@@ -7,7 +7,7 @@ Set Default Proof Using "Type".
(** Moving a read of a mutable reference down across code that *may* use that ref. *)
(* Assuming x : &mut i32 *)
Definition ex1_down : function :=
Definition ex1_down_unopt : function :=
fun: ["i"],
let: "x" := new_place (&mut int) "i" in (* put argument into place *)
retag_place "x" (RefPtr Mutable) int FnEntry ;;
......@@ -27,7 +27,7 @@ Definition ex1_down_opt : function :=
"v"
.
Lemma ex1_down_sim_fun : ⊨ᶠ ex1_down ex1_down_opt.
Lemma ex1_down_sim_fun : ⊨ᶠ ex1_down_unopt ex1_down_opt.
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.
......@@ -60,10 +60,10 @@ Proof.
sim_apply sim_body_retag_ref_fn_entry; [simpl; lia|eauto| |done|..].
{ rewrite -cmra_assoc (cmra_comm (res_cs _ _)) cmra_assoc. eauto. }
{ eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
move=> l' told tnew hplt α' nxtp' r0 ? _ IS_i σs2 σt2 s_new tk _ /=.
move=> l' told tnew hplt α' nxtp' r0 ? _ IS_i InD σs2 σt2 s_new tk _ /=.
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 & Eqss & Eqst & ARELs) TOP].
have IS_O := (IS_i O ltac:(simpl; lia)). rewrite shift_loc_0_nat in IS_O.
destruct IS_O as [(ss & st & Eql' & Eqss & Eqst & ARELs) TOP].
rewrite insert_empty.
(* Write local *)
sim_apply sim_body_write_local_1; [solve_sim..|].
......@@ -92,16 +92,60 @@ Proof.
sim_apply_r sim_body_deref_r =>/=.
sim_apply_r sim_body_copy_protected_r;
[solve_sim..|by rewrite lookup_insert|by eapply elem_of_dom_2|].
apply: sim_body_result=>_ /=.
intros Eqss3 Eqst3.
apply: sim_body_result=> Hval /=.
apply: sim_body_let_r=>/=.
(* Free stuff *)
sim_apply sim_body_free_unique_local_1;
[done|rewrite /res_loc /= insert_empty; solve_sim |by left|].
simpl => _ _ α4 _.
move => _ _ α4 _ σs4 σt4.
sim_apply sim_body_let=>/=.
(* Remove protection *)
set r1 := rarg r0 res_cs (snc σt) {[tnew := dom (gset loc) hplt]}
res_tag tnew tk hplt rf'.
set r2 := rarg r0 res_cs (snc σt) res_tag tnew tk hplt rf'.
rewrite (_: rarg res_cs (snc σt) {[tnew := dom (gset loc) hplt]}
res_tag tnew tk hplt r0 rf' r1); last first.
{ rewrite -cmra_assoc (cmra_comm r0 rf') cmra_assoc (cmra_comm _ r0)
!cmra_assoc (cmra_comm r0) //. }
apply (viewshift_state_sim_local_body _ _ _ _ r1 r2).
{ rewrite /r1 /r2. do 2 apply viewshift_state_frame_r.
rewrite -insert_empty. 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 => ss4 /= /lookup_delete_Some [? Eqst4].
rewrite Eqst4 in Eqst3. simplify_eq. exists ss.
rewrite lookup_delete_ne; [|done]. split; [done|].
move : ARELs. apply arel_mono; [|solve_res]. clear -Hval.
apply (cmra_valid_included _ _ Hval).
do 2 (etrans; [|apply cmra_included_l]).
apply cmra_mono_r. solve_res. } clear Hval.
(* Finishing up. *)
apply: sim_body_result => Hval. split.
- exists σt.(snc). split; [done|]. admit.
- exists σt.(snc). split; [done|]. rewrite /end_call_sat.
apply (cmap_lookup_op_unique_included (res_cs (snc σt) ).(rcm));
[apply Hval|apply prod_included; rewrite /r2; solve_res|..].
by rewrite res_cs_lookup.
- constructor; [|by constructor].
move : ARELs. apply arel_mono; [done|solve_res].
Abort.
move : ARELs. rewrite /r2. apply arel_mono; [done|solve_res].
Qed.
(** Top-level theorem: Two programs that only differ in the
"ex1_down" function are related. *)
Corollary ex1_down (prog: fn_env) :
stuck_decidable
prog_wf prog
let prog_src := <["ex1_down":=ex1_down_unopt]> prog in
let prog_tgt := <["ex1_down":=ex1_down_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: ex1_down_sim_fun.
- exact: sim_mod_funs_refl.
Qed.
Print Assumptions ex1_down.
......@@ -215,6 +215,15 @@ Proof.
by apply (cmap_lookup_op_unique_included r1.(rcm)).
Qed.
Lemma pub_loc_mono (r1 r2 : resUR) (VAL: r2) :
r1 r2 l σs σt, pub_loc r1 l σs σt pub_loc r2 l σs σt.
Proof.
intros LE l σs σt PUB st Eqst.
destruct (PUB _ Eqst) as (ss & Eqss & AREL).
exists ss. split; [done|].
by eapply arel_mono.
Qed.
Instance tmap_inv_proper : Proper (() ==> (=) ==> (=) ==> iff) tmap_inv.
Proof.
intros r1 r2 [Eqt Eqc] ? σ ? ???. subst. rewrite /tmap_inv.
......
......@@ -1681,6 +1681,7 @@ Lemma sim_body_retag_ref_fn_entry n fs ft mut r r' c cids Ts ptr T σs σt Φ :
σs.(shp) !! (l + i) = Some ss σt.(shp) !! (l + i) = Some st
arel r0 ss st)
tag_on_top α' (l + i) tnew pm)
( l', l' dom (gset loc) hplt i : nat, (i < tsize T)%nat l' = l + i)
let σs' := mkState σs.(shp) α' σs.(scs) nxtp' σs.(snc) in
let σt' := mkState σt.(shp) α' σt.(scs) nxtp' σt.(snc) in
let s_new := ScPtr l (Tagged tnew) in
......@@ -1978,6 +1979,7 @@ Proof.
destruct mut.
* eapply tag_on_top_retag_ref_uniq. exact EqRT.
* eapply tag_on_top_retag_ref_shr; [done|exact EqRT].
- move => ? /write_hpl_elem_of_dom_from_empty. by rewrite EqlT.
- destruct mut; [done|]. simpl. do 2 (split; [done|]).
rewrite lookup_insert. by eexists.
Qed.
......
......@@ -227,7 +227,8 @@ Lemma sim_body_copy_protected_r
h !! l = Some (ss, st)
Ts !! t = Some L
l L
(r {n,fs,ft} (es, σs) (#[st], σt) : Φ : Prop)
(σs.(shp) !! l = Some ss σt.(shp) !! l = Some 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 Eqr Eqr' Eqs EqTs InL CONT. pfold.
......@@ -298,7 +299,7 @@ Proof.
by destruct σt. rewrite Eqσt. rewrite Eqσt in STEPT'. clear Eqσt.
exists es, σs, r, n. split; last split; [|done|].
- right. split; [lia|done].
- by left.
- left. by apply CONT.
Qed.
End right.
......@@ -18,52 +18,60 @@ Lemma viewshift_state_frame_r r r1 r2 σs σt :
r1 |={σs,σt}=> r2 (r1 r) |={σs,σt}=> (r2 r).
Proof. intros VS ?. rewrite (cmra_comm r1) (cmra_comm r2) 2!cmra_assoc. apply VS. Qed.
(* Lemma vs_call_empty_public c :
res_cs c (csOwned ) |==> res_cs c csPub.
Lemma vs_state_drop_protector r c t L Ts σs σt
(HN: Ts !! t = None)
(REL: l, l L pub_loc r l σs σt) :
r res_cs c (<[t := L]> Ts) |={σs, σt}=> r res_cs c Ts.
Proof.
intros r_f σs σt.
intros (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
have EQtm: (r_f res_cs c (csOwned )).(rtm)
(r_f res_cs c csPub).(rtm) by done.
have EQlm: (r_f res_cs c (csOwned )).(rlm)
(r_f res_cs c csPub).(rlm) by done.
have UNIQUE: r_f.(rcm) !! c = None.
{ move : (proj2 (proj1 VALID) c). rewrite lookup_op.
destruct (r_f.(rcm) !! c) as [cs|] eqn:Eqcs; [|done].
rewrite Eqcs /= lookup_insert -Some_op.
intros r_f. rewrite 2!cmra_assoc.
intros (WFS & WFT & VALID & PINV & CINV & SREL).
have EQtm: (r_f r res_cs c (<[t := L]> Ts)).(rtm)
(r_f r res_cs c Ts).(rtm) by done.
have UNIQUE: (r_f r).(rcm) !! c = None.
{ destruct ((r_f r).(rcm) !! c) eqn:Eqcs; [|done].
move : (proj2 VALID c). rewrite lookup_op.
rewrite Eqcs res_cs_lookup -Some_op.
intros ?%exclusive_r; [done|apply _]. }
have EQO: (r_f res_cs c (csOwned )).(rcm) !! c Some $ to_callStateR (csOwned ).
{ rewrite lookup_op UNIQUE left_id /= lookup_insert //. }
split; last split; last split; last split; last split; last split;
[done|done|..].
- apply (local_update_discrete_valid_frame _ _ _ VALID).
rewrite (cmra_comm r_f) (cmra_comm _ (res_cs _ csPub)).
apply prod_local_update_1, prod_local_update_2.
rewrite /= -insert_singleton_op // -insert_singleton_op //.
rewrite -(insert_insert _ c (Cinr ()) (Cinl (Excl ))).
eapply singleton_local_update; [by rewrite lookup_insert|].
by apply exclusive_local_update.
- intros t k h. rewrite -EQtm. intros Eqkh. by apply PINV.
- intros c' cs'. case (decide (c' = c)) => ?; [subst c'|].
+ rewrite lookup_op UNIQUE left_id /= lookup_insert.
intros Eq%Some_equiv_inj.
specialize (CINV _ _ EQO) as [IN _].
have Lt := state_wf_cid_agree _ WFT _ IN.
destruct cs' as [[]| |]; try inversion Eq. done.
+ intros EQcs. apply (CINV c' cs').
move : EQcs. rewrite 2!lookup_op lookup_insert_ne // lookup_insert_ne //.
have EQO: (r_f r res_cs c (<[t := L]> Ts)).(rcm) !! c Excl' (<[t := L]> Ts).
{ by rewrite lookup_op UNIQUE left_id res_cs_lookup. }
have VALID': (r_f r res_cs c Ts).
{ by apply (local_update_discrete_valid_frame _ _ _ VALID), res_cs_local_update. }
split; last split; last split; last split; last split; [done|done|done|..].
- intros ???. rewrite -EQtm. apply PINV.
- intros c1 Ts1.
case (decide (c1 = c)) => ?; [subst c1|].
+ rewrite lookup_op UNIQUE left_id res_cs_lookup.
intros Eq%Some_equiv_inj%Excl_inj%leibniz_equiv_iff. subst Ts1.
specialize (CINV _ _ EQO) as [IN CINV].
split; [done|]. intros t1 L1 Eq1.
apply CINV. rewrite lookup_insert_ne; [done|].
intros ?. subst t1. by rewrite HN in Eq1.
+ intros EQcs. apply (CINV c1 Ts1).
rewrite lookup_op res_cs_lookup_ne; [|done].
move : EQcs. by rewrite lookup_op res_cs_lookup_ne.
- destruct SREL as (?&?&?&?& PB). do 4 (split; [done|]).
intros l InD. specialize (PB _ InD) as [PB|(t & h & Eqh & PV)]; [left|right].
+ intros st Eqst. specialize (PB _ Eqst) as (ss & ? & AREL).
by exists ss.
+ exists t, h. rewrite -EQtm -EQlm. split; [done|].
destruct PV as [?|(c' & T' & Eqc' & InT & ?)]; [by left|right].
exists c', T'. split; [|done].
have ? : c' c.
{ intros ?. subst c'. move : Eqc'.
rewrite lookup_op /= lookup_insert. intros ?%callStateR_exclusive_eq.
subst T'. by apply not_elem_of_empty in InT. }
move : Eqc'.
rewrite 2!lookup_op lookup_insert_ne // lookup_insert_ne //.
- intros l. setoid_rewrite <-EQlm. by specialize (LINV l).
Qed. *)
intros l InD.
specialize (PB _ InD) as [PB|(t1 & k1 & h1 & Eq1 & IS1 & PV)]; [by left|].
rewrite ->EQtm in Eq1.
destruct PV as [|(Eqk1 & c1 & T1 & L1 & Eqc1 & EqT1 & InL1)].
{ right. exists t1, k1, h1. do 2 (split; [done|]); by left. }
case (decide (c1 = c)) => ?; [subst c1|].
+ move : Eqc1. rewrite lookup_op UNIQUE res_cs_lookup left_id.
intros ?%Some_equiv_inj%Excl_inj%leibniz_equiv_iff. subst T1.
case (decide (t1 = t)) => ?; [subst t1|].
* left. eapply pub_loc_mono; [done|..|apply REL].
{ etrans; [|apply cmra_included_l]. apply cmra_included_r. }
{ clear - EqT1 InL1. move : EqT1.
rewrite lookup_insert. intros. by simplify_eq. }
* right. exists t1, k1, h1. do 2 (split; [done|]).
right. split; [done|]. exists c, Ts, L1. split; last split; [..|done].
{ by rewrite lookup_op UNIQUE res_cs_lookup left_id. }
{ move : EqT1. by rewrite lookup_insert_ne. }
+ right. exists t1, k1, h1. do 2 (split; [done|]).
right. split; [done|]. exists c1, T1, L1. split; [|done].
rewrite lookup_op res_cs_lookup_ne; [|done].
move : Eqc1. by rewrite lookup_op res_cs_lookup_ne.
Qed.
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