ex1.v 4.14 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
15
    Retag "x" Default ;;
    Call #[ScFnPtr "f"] [] ;;
    *{int} "x" <- #[42] ;;
    Call #[ScFnPtr "g"] [] ;;
    Copy *{int} "x"
Hai Dang's avatar
Hai Dang committed
16
17
  .

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

Ralf Jung's avatar
Ralf Jung committed
29
30
Lemma ex1_sim_body :
  ⊨ᶠ ex1_unopt  ex1_opt.
Hai Dang's avatar
Hai Dang committed
31
Proof.
Ralf Jung's avatar
Ralf Jung committed
32
  apply (sim_fun_simple1 10)=>// fs ft rarg es css et cs args argt LOOK AREL ??.
33
  simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
34
  (* InitCall *)
Ralf Jung's avatar
Ralf Jung committed
35
  apply sim_simple_init_call=> c /= {css}.
Ralf Jung's avatar
Ralf Jung committed
36
  (* Alloc local *)
Ralf Jung's avatar
Ralf Jung committed
37
  sim_apply sim_simple_alloc_local=> l t /=.
Ralf Jung's avatar
Ralf Jung committed
38
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
39
  (* Write local *)
Ralf Jung's avatar
Ralf Jung committed
40
  rewrite (vrel_eq _ _ _ AREL).
Ralf Jung's avatar
Ralf Jung committed
41
  sim_apply sim_simple_write_local; [solve_sim..|].
Ralf Jung's avatar
Ralf Jung committed
42
  intros arg ->. simpl.
Ralf Jung's avatar
Ralf Jung committed
43
44
  sim_apply sim_simple_let=>/=.
  apply: sim_simple_result.
Ralf Jung's avatar
Ralf Jung committed
45
  (* Retag local *)
Ralf Jung's avatar
Ralf Jung committed
46
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
47
48
49
  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.
Ralf Jung's avatar
Ralf Jung committed
50
  sim_apply sim_simple_retag_local; [solve_sim..|].
Ralf Jung's avatar
Ralf Jung committed
51
52
  move=>l_i tg_i hplt /= Hl_i.
  (* Call *)
Ralf Jung's avatar
Ralf Jung committed
53
54
55
56
57
  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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
  (* 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 Hσs Hσt. 
  sim_apply sim_body_write_owned; [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..|].
Ralf Jung's avatar
Ralf Jung committed
73
  { subst σt'. eapply steps_retag.tag_on_top_write; done. }
Ralf Jung's avatar
Ralf Jung committed
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
  { 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. { intros ?????? HH. exact HH. }
  simplify_eq/=. rewrite Hσs Hσt. 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 Hσs Hσ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. }
Ralf Jung's avatar
Ralf Jung committed
93
94
  (* Finishing up. *)
  eapply sim_body_viewshift.
Hai Dang's avatar
Hai Dang committed
95
  { do 5 eapply viewshift_frame_r. eapply vs_call_empty_public. }
96
  apply: sim_body_result=>Hval. simpl. split.
Ralf Jung's avatar
Ralf Jung committed
97
98
  - eexists. split; first done. eapply res_end_call_sat; first done.
    solve_res.
Ralf Jung's avatar
Ralf Jung committed
99
  - constructor; simpl; auto.
Ralf Jung's avatar
Ralf Jung committed
100
Qed.
Ralf Jung's avatar
Ralf Jung committed
101

Ralf Jung's avatar
Ralf Jung committed
102
103
(** Top-level theorem: Two programs that only differ in the
"ex1" function are related. *)
Ralf Jung's avatar
Ralf Jung committed
104
Corollary ex1 (prog: fn_env) :
Ralf Jung's avatar
Ralf Jung committed
105
  stuck_decidable 
Ralf Jung's avatar
Ralf Jung committed
106
  prog_wf prog 
Ralf Jung's avatar
Ralf Jung committed
107
  let prog_src := <["ex1":=ex1_unopt]> prog in
Ralf Jung's avatar
Ralf Jung committed
108
109
110
  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
111
  intros Hdec Hwf. apply sim_prog_sim_classical.
Ralf Jung's avatar
Ralf Jung committed
112
  { apply Hdec. }
Ralf Jung's avatar
Ralf Jung committed
113
  { apply has_main_insert, Hwf; done. }
Ralf Jung's avatar
Ralf Jung committed
114
115
  apply sim_mod_funs_local.
  apply sim_mod_funs_insert; first done.
Ralf Jung's avatar
Ralf Jung committed
116
  - exact: ex1_sim_body.
Ralf Jung's avatar
Ralf Jung committed
117
118
  - exact: sim_mod_funs_refl.
Qed.
Ralf Jung's avatar
Ralf Jung committed
119
120

Print Assumptions ex1.