ex1.v 4.56 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stbor.sim Require Import local invariant refl tactics simple program refl_step right_step left_step viewshift.
Hai Dang's avatar
Hai Dang committed
2 3 4

Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
5 6
(** Moving read of mutable reference up across code not using that ref. *)

Hai Dang's avatar
Hai Dang committed
7
(* Assuming x : &mut i32 *)
Ralf Jung's avatar
Ralf Jung committed
8
Definition ex1_unopt : function :=
Hai Dang's avatar
Hai Dang committed
9
  fun: ["i"],
Ralf Jung's avatar
Ralf Jung committed
10
    let: "x" := new_place (&mut int) "i" in (* put argument into place *)
Hai Dang's avatar
Hai Dang committed
11 12 13 14
    Retag "x" Default ;;
    Call #[ScFnPtr "f"] [] ;;
    *{int} "x" <- #[42] ;;
    Call #[ScFnPtr "g"] [] ;;
Ralf Jung's avatar
Ralf Jung committed
15 16 17
    let: "v" := Copy *{int} "x" in
    Free "x" ;; Free "i" ;;
    "v"
Hai Dang's avatar
Hai Dang committed
18 19
  .

Hai Dang's avatar
Hai Dang committed
20 21
Definition ex1_opt : function :=
  fun: ["i"],
Ralf Jung's avatar
Ralf Jung committed
22
    let: "x" := new_place (&mut int) "i" in
Hai Dang's avatar
Hai Dang committed
23 24 25 26 27
    Retag "x" Default ;;
    Call #[ScFnPtr "f"] [] ;;
    *{int} "x" <- #[42] ;;
    let: "v" := Copy *{int} "x" in
    Call #[ScFnPtr "g"] [] ;;
Ralf Jung's avatar
Ralf Jung committed
28
    Free "x" ;; Free "i" ;;
Hai Dang's avatar
Hai Dang committed
29
    "v"
Hai Dang's avatar
Hai Dang committed
30 31
  .

Ralf Jung's avatar
Ralf Jung committed
32 33
Lemma ex1_sim_body :
  ⊨ᶠ ex1_unopt  ex1_opt.
Hai Dang's avatar
Hai Dang committed
34
Proof.
35
  apply (sim_fun_simple1 10)=>// fs ft rarg es et args argt c LOOK AREL ??.
36
  simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
37
  (* Alloc local *)
Ralf Jung's avatar
Ralf Jung committed
38
  sim_apply sim_simple_alloc_local=> l t /=.
Ralf Jung's avatar
Ralf Jung committed
39
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
40
  (* Write local *)
Ralf Jung's avatar
Ralf Jung committed
41
  rewrite (vrel_eq _ _ _ AREL).
Ralf Jung's avatar
Ralf Jung committed
42
  sim_apply sim_simple_write_local; [solve_sim..|].
Hai Dang's avatar
Hai Dang committed
43
  intros sarg ->.
Ralf Jung's avatar
Ralf Jung committed
44 45
  sim_apply sim_simple_let=>/=.
  apply: sim_simple_result.
Ralf Jung's avatar
Ralf Jung committed
46
  (* Retag local *)
Ralf Jung's avatar
Ralf Jung committed
47
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
48 49 50
  destruct args as [|args args']; first by inversion AREL.
  apply Forall2_cons_inv in AREL as [AREL ATAIL].
  destruct args' as [|]; last by inversion ATAIL. clear ATAIL.
Hai Dang's avatar
Hai Dang committed
51
  sim_apply sim_simple_retag_local; [simpl; lia|solve_sim..|].
Ralf Jung's avatar
Ralf Jung committed
52 53
  move=>l_i tg_i hplt /= Hl_i.
  (* Call *)
Ralf Jung's avatar
Ralf Jung committed
54 55 56 57 58
  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=>/=.
Ralf Jung's avatar
Ralf Jung committed
59 60 61 62 63
  (* 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. *)
64
  intros σs σt.
Hai Dang's avatar
Hai Dang committed
65 66
  sim_apply sim_body_write_unique_1; [solve_sim..|].
  intros ?? Htop. simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
67 68 69 70 71 72 73 74 75 76 77
  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! *)
Ralf Jung's avatar
Ralf Jung committed
78
  eapply (sim_simplify (fun_post_simple c)). { by eauto. }
79
  simplify_eq/=. clear- AREL FREL LOOK.
Ralf Jung's avatar
Ralf Jung committed
80 81 82 83 84 85
  (* 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. *)
86
  intros σs σt.
Ralf Jung's avatar
Ralf Jung committed
87 88 89 90 91 92
  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. }
Ralf Jung's avatar
Ralf Jung committed
93 94 95 96
  apply: sim_body_result=>Hval. simpl.
  apply: sim_body_let_l. simpl.
  (* Free stuff *)
  eapply (sim_simplify (fun_post_simple c)). { by eauto. }
Hai Dang's avatar
Hai Dang committed
97
  sim_apply sim_simple_free_local_1; [try solve_sim..|]. simpl.
Ralf Jung's avatar
Ralf Jung committed
98
  sim_apply sim_simple_let=>/=.
Hai Dang's avatar
Hai Dang committed
99 100 101 102 103 104
  sim_apply sim_simple_free_public.
  { simpl. constructor; [|by constructor].
    assert (args = sarg). { by revert AREL; apply arel_eq. } subst args.
    revert AREL. apply arel_mono; [|solve_res].
    apply (cmra_valid_included _ _ Hval).
    do 3 apply cmra_mono_r. apply cmra_included_l. } simpl.
Ralf Jung's avatar
Ralf Jung committed
105
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
106
  (* Finishing up. *)
Hai Dang's avatar
Hai Dang committed
107 108
  (* eapply sim_body_viewshift.
  { do 5 eapply viewshift_frame_r. eapply vs_call_empty_public. } *)
Ralf Jung's avatar
Ralf Jung committed
109
  apply: sim_simple_result. split.
110
  - solve_res.
Ralf Jung's avatar
Ralf Jung committed
111
  - constructor; simpl; auto.
Hai Dang's avatar
Hai Dang committed
112
Qed.
Ralf Jung's avatar
Ralf Jung committed
113

Ralf Jung's avatar
Ralf Jung committed
114 115
(** Top-level theorem: Two programs that only differ in the
"ex1" function are related. *)
Ralf Jung's avatar
Ralf Jung committed
116
Corollary ex1 (prog: fn_env) :
Ralf Jung's avatar
Ralf Jung committed
117
  stuck_decidable 
Ralf Jung's avatar
Ralf Jung committed
118
  prog_wf prog 
Ralf Jung's avatar
Ralf Jung committed
119
  let prog_src := <["ex1":=ex1_unopt]> prog in
Ralf Jung's avatar
Ralf Jung committed
120 121 122
  let prog_tgt := <["ex1":=ex1_opt]> prog in
  behave_prog prog_tgt <1= behave_prog prog_src.
Proof.
Ralf Jung's avatar
Ralf Jung committed
123
  intros Hdec Hwf. apply sim_prog_sim_classical.
Ralf Jung's avatar
Ralf Jung committed
124
  { apply Hdec. }
Ralf Jung's avatar
Ralf Jung committed
125
  { apply has_main_insert, Hwf; done. }
Ralf Jung's avatar
Ralf Jung committed
126 127
  apply sim_mod_funs_local.
  apply sim_mod_funs_insert; first done.
Ralf Jung's avatar
Ralf Jung committed
128
  - exact: ex1_sim_body.
Ralf Jung's avatar
Ralf Jung committed
129 130
  - exact: sim_mod_funs_refl.
Qed.
Ralf Jung's avatar
Ralf Jung committed
131 132

Print Assumptions ex1.