ex1.v 4 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.
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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
  (* 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..|].
  { subst σt'. admit. (* show that tag_op_top is preserved. *) }
  { 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. }
93
  apply: sim_body_result=>Hval. simpl. split.
Ralf Jung's avatar
Ralf Jung committed
94
95
  - eexists. split; first done. admit. (* end_call_sat *)
  - constructor; simpl; auto.
Ralf Jung's avatar
Ralf Jung committed
96
97
Admitted.

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

Print Assumptions ex1.