Commit 53670eed authored by Hai Dang's avatar Hai Dang

WIP: ex1_down

parent 64421169
......@@ -13,7 +13,7 @@ Definition ex1_unopt : function :=
*{int} "x" <- #[42] ;;
Call #[ScFnPtr "g"] [] ;;
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
......@@ -25,7 +25,7 @@ Definition ex1_opt : function :=
*{int} "x" <- #[42] ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "g"] [] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
......@@ -104,12 +104,6 @@ Proof.
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.
......
......@@ -13,9 +13,9 @@ Definition ex1_down : function :=
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
.
Definition ex1_down_opt : function :=
fun: ["i"],
......@@ -23,9 +23,9 @@ Definition ex1_down_opt : function :=
retag_place "x" (RefPtr Mutable) int FnEntry ;;
Call #[ScFnPtr "f"] [] ;;
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
.
Lemma ex1_down_sim_fun : ⊨ᶠ ex1_down ex1_down_opt.
Proof.
......@@ -63,7 +63,8 @@ Proof.
move=> l' told tnew hplt α' nxtp' r0 ? _ IS_i σ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) TOP].
destruct IS_i as [(ss & st & IS_i & Eqss & Eqst & ARELs) TOP].
rewrite insert_empty.
(* Write local *)
sim_apply sim_body_write_local_1; [solve_sim..|].
intros s ?. simplify_eq. simpl.
......@@ -77,8 +78,9 @@ Proof.
apply: sim_body_result=>_ /=.
apply: sim_body_let_l=>/=.
(* Call *)
rewrite -(right_id ε op ( _ res_loc _ _ _)).
sim_apply (sim_body_step_over_call _ _ _ ε _ (ValR _) [] []); [constructor|done|..].
rewrite -(right_id ε op (_ res_loc _ _ _)).
sim_bind (Call _ _) (Call _ _). (* TODO: sim_apply fails to instantiate evars *)
apply (sim_body_step_over_call _ _ _ ε _ (ValR _) [] []); [solve_sim..|].
move => rf' ? _ _ frs' frt' σs3 σt3 _ /= Eqs1 Eqs2 ? _ _. simplify_eq.
exists 5%nat.
apply: sim_body_result=>_ /=.
......@@ -90,6 +92,16 @@ 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=>Hval /=.
apply: sim_body_result=>_ /=.
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 _.
sim_apply sim_body_let=>/=.
(* Finishing up. *)
apply: sim_body_result => Hval. split.
- exists σt.(snc). split; [done|]. admit.
- constructor; [|by constructor].
move : ARELs. apply arel_mono; [done|solve_res].
Abort.
......@@ -12,7 +12,7 @@ Definition ex2_unopt : function :=
retag_place "x" (RefPtr Immutable) int Default ;;
Call #[ScFnPtr "f"] [Copy "x"] ;;
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
......@@ -22,7 +22,7 @@ Definition ex2_opt : function :=
retag_place "x" (RefPtr Immutable) int Default ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] [Copy "x"] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
......@@ -50,7 +50,7 @@ Proof.
(* 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
move=> l' told tnew hplt c' cids α' nxtp' r0 ? _ _ 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].
......@@ -73,9 +73,9 @@ Proof.
sim_apply sim_simple_copy_local; [solve_sim..|].
apply: sim_simple_result. simpl.
(* Call *)
rewrite (_: rarg res_cs c res_tag tnew tk hplt
rewrite (_: rarg res_cs c res_tag tnew tk hplt r0
res_loc l [(ScPtr l' (Tagged tnew), ScPtr l' (Tagged tnew))] t
rarg res_cs c res_tag tnew tk hplt
rarg res_cs c res_tag tnew tk hplt r0
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. }
......@@ -101,12 +101,6 @@ Proof.
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.
......
......@@ -13,9 +13,9 @@ Definition ex2_down : function :=
retag_place "x" (RefPtr Immutable) int FnEntry ;;
let: "v" := Copy *{int} "x" in
Call #[ScFnPtr "f"] [Copy "x"] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
.
Definition ex2_down_opt : function :=
fun: ["i"],
......@@ -23,9 +23,9 @@ Definition ex2_down_opt : function :=
retag_place "x" (RefPtr Immutable) int FnEntry ;;
Call #[ScFnPtr "f"] [Copy "x"] ;;
let: "v" := Copy *{int} "x" in
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
.
Lemma ex2_down_sim_fun : ⊨ᶠ ex2_down ex2_down_opt.
......
......@@ -13,7 +13,7 @@ Definition ex3 : function :=
*{int} "x" <- #[42] ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
......@@ -23,8 +23,9 @@ Definition ex3_opt_1 : function :=
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[42] ;;
*{int} "x" <- #[13] ;;
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i"
let: "v" := Call #[ScFnPtr "f"] [] in
Free "x" ;;
"v"
.
Definition ex3_opt_2 : function :=
......@@ -32,8 +33,9 @@ Definition ex3_opt_2 : function :=
let: "x" := new_place (&mut int) "i" in
retag_place "x" (RefPtr Mutable) int FnEntry ;;
*{int} "x" <- #[13] ;;
Call #[ScFnPtr "f"] [] ;;
Free "x" ;; Free "i"
let: "v" := Call #[ScFnPtr "f"] [] in
Free "x" ;;
"v"
.
Lemma ex3_sim_fun : ⊨ᶠ ex3 ex3_opt_1.
......
......@@ -12,7 +12,7 @@ Definition ex3_down : function :=
*{int} "x" <- #[42] ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
......@@ -23,7 +23,7 @@ Definition ex3_down_opt_1 : function :=
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[42] ;;
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
......@@ -33,9 +33,9 @@ Definition ex3_down_opt_2 : function :=
retag_place "x" (RefPtr Mutable) int FnEntry ;;
let: "v" := Call #[ScFnPtr "f"] [] in
*{int} "x" <- #[13] ;;
Free "x" ;; Free "i" ;;
Free "x" ;;
"v"
.
.
Lemma ex3_down_sim_fun : ⊨ᶠ ex3_down ex3_down_opt_1.
Proof.
......
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