ex1.v 6.18 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"],
Hai Dang's avatar
Hai Dang committed
10 11 12 13
    (* "x" is the local variable that stores the pointer value "i" *)
    let: "x" := new_place (&mut int) "i" in

    (* retag_place reborrows the pointer value stored in "x" (which is "i"),
Ralf Jung's avatar
Ralf Jung committed
14 15
      then updates "x" with the new pointer value.  A [Default] retag is
      sufficient for this, we don't need the protector. *)
Hai Dang's avatar
Hai Dang committed
16
    retag_place "x" (RefPtr Mutable) int Default ;;
Hai Dang's avatar
Hai Dang committed
17 18

    (* The unknown code is represented by a call to an unknown function "f" or
Ralf Jung's avatar
Ralf Jung committed
19
      "g". *)
Hai Dang's avatar
Hai Dang committed
20
    Call #[ScFnPtr "f"] [] ;;
Hai Dang's avatar
Hai Dang committed
21 22

    (* Write 42 to the cell pointed to by the pointer in "x" *)
Hai Dang's avatar
Hai Dang committed
23
    *{int} "x" <- #[42] ;;
Hai Dang's avatar
Hai Dang committed
24

Hai Dang's avatar
Hai Dang committed
25
    Call #[ScFnPtr "g"] [] ;;
Hai Dang's avatar
Hai Dang committed
26 27

    (* Read the value "v" from the cell pointed to by the pointer in "x" *)
Ralf Jung's avatar
Ralf Jung committed
28
    let: "v" := Copy *{int} "x" in
Hai Dang's avatar
Hai Dang committed
29 30

    (* Free the local variable *)
Hai Dang's avatar
Hai Dang committed
31
    Free "x" ;;
Hai Dang's avatar
Hai Dang committed
32 33

    (* Finally, return the read value *)
Ralf Jung's avatar
Ralf Jung committed
34
    "v"
Hai Dang's avatar
Hai Dang committed
35 36
  .

Hai Dang's avatar
Hai Dang committed
37 38
Definition ex1_opt : function :=
  fun: ["i"],
Ralf Jung's avatar
Ralf Jung committed
39
    let: "x" := new_place (&mut int) "i" in
Hai Dang's avatar
Hai Dang committed
40
    retag_place "x" (RefPtr Mutable) int Default ;;
Hai Dang's avatar
Hai Dang committed
41 42 43 44
    Call #[ScFnPtr "f"] [] ;;
    *{int} "x" <- #[42] ;;
    let: "v" := Copy *{int} "x" in
    Call #[ScFnPtr "g"] [] ;;
Hai Dang's avatar
Hai Dang committed
45
    Free "x" ;;
Hai Dang's avatar
Hai Dang committed
46
    "v"
Hai Dang's avatar
Hai Dang committed
47 48
  .

49 50
(** A sketch of this proof is given in Section 3.4 of the Stacked Borrows paper.
  Here the expressions are calling unknown functions "f" and "g". *)
Hai Dang's avatar
Hai Dang committed
51
Lemma ex1_sim_fun :
Ralf Jung's avatar
Ralf Jung committed
52
  ⊨ᶠ ex1_unopt  ex1_opt.
Hai Dang's avatar
Hai Dang committed
53
Proof.
Ralf Jung's avatar
Ralf Jung committed
54
  apply (sim_fun_simple1 10)=>// fs ft rarg es et arg c LOOK AREL ??.
55
  simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
56
  (* Alloc local *)
Ralf Jung's avatar
Ralf Jung committed
57
  sim_apply sim_simple_alloc_local=> l t /=.
Ralf Jung's avatar
Ralf Jung committed
58
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
59
  (* Write local *)
Ralf Jung's avatar
Ralf Jung committed
60
  sim_apply sim_simple_write_local; [solve_sim..|].
Hai Dang's avatar
Hai Dang committed
61
  intros sarg ->.
Ralf Jung's avatar
Ralf Jung committed
62 63
  sim_apply sim_simple_let=>/=.
  apply: sim_simple_result.
Ralf Jung's avatar
Ralf Jung committed
64
  (* ## Step (1) in the proof sketch:
65
      retagging with a fresh tag `tg_n` on top of "x"'s stack. *)
Hai Dang's avatar
Hai Dang committed
66
  (* Retag a local place *)
Ralf Jung's avatar
Ralf Jung committed
67
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
68
  apply Forall2_cons_inv in AREL as [AREL _].
Hai Dang's avatar
Hai Dang committed
69 70 71
  sim_apply sim_simple_let=>/=.
    (* Copy local place *)
    sim_apply sim_simple_copy_local; [solve_sim..|].
Hai Dang's avatar
Hai Dang committed
72
    apply sim_simple_valid_post.
Hai Dang's avatar
Hai Dang committed
73
    apply: sim_simple_result=> VALID /=.
Hai Dang's avatar
Hai Dang committed
74
    (* Retag *)
Hai Dang's avatar
Hai Dang committed
75
    sim_apply sim_simple_retag_ref; [simpl; lia|done| |eauto|..].
Hai Dang's avatar
Hai Dang committed
76
    { eapply arel_mono; [done|..|exact AREL]. solve_res. } clear VALID.
Hai Dang's avatar
Hai Dang committed
77
    move=>l_i tg_i tg_n hplt /= ?? IS_i. subst sarg.
Hai Dang's avatar
Hai Dang committed
78 79 80 81
    specialize (IS_i O ltac:(lia)). rewrite shift_loc_0_nat in IS_i.
    (* Write local *)
    sim_apply sim_simple_write_local; [solve_sim..|].
    intros s ?. simplify_eq.
82
  (* Call unknown function "f" *)
Ralf Jung's avatar
Ralf Jung committed
83 84 85
  sim_apply sim_simple_let=>/=.
  sim_apply (sim_simple_call 10 [] [] ε); [solve_sim..|].
  intros rf frs frt ??? ? _ _ FREL. simplify_eq/=.
Hai Dang's avatar
Hai Dang committed
86
  apply: sim_simple_result=>/=.
Ralf Jung's avatar
Ralf Jung committed
87
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
88 89
  (* Copy local *)
  sim_apply sim_simple_copy_local; [solve_sim..|].
Hai Dang's avatar
Hai Dang committed
90
  apply: sim_simple_result=>/=.
Ralf Jung's avatar
Ralf Jung committed
91 92
  sim_apply sim_simple_deref=>l' t' ?. simplify_eq/=.
  (* Write unique. We need to drop to complex mode, to preserve some local state info. *)
93
  intros σs σt.
Hai Dang's avatar
Hai Dang committed
94 95
  sim_apply sim_body_write_unique_1; [solve_sim..|].
  intros ?? Htop. simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
96
  sim_apply sim_body_let. simplify_eq/=.
Ralf Jung's avatar
Ralf Jung committed
97
  (* ## Step (2) in the proof sketch:
98 99 100 101 102
      If "x" had been accessed by "f", then "f" must have use a tag different
      from `tg_n`, which in turn implies that `tg_n` would have been popped off
      "x"'s stack. However, since the write `*{int} "x" <- #[42]` does not have
      undefined behavior, "f" must not have accessed "x", and "x"'s stack must
      have remained unchanged. *)
Ralf Jung's avatar
Ralf Jung committed
103 104
  (* Copy local (right) *)
  sim_apply_r sim_body_copy_local_r; [solve_sim..|].
Hai Dang's avatar
Hai Dang committed
105
  apply: sim_body_result=>_/=.
Ralf Jung's avatar
Ralf Jung committed
106
  (* Copy unique (right) *)
Hai Dang's avatar
Hai Dang committed
107
  sim_apply_r sim_body_deref_r=>/=.
Ralf Jung's avatar
Ralf Jung committed
108 109
  sim_apply_r sim_body_copy_unique_r; [try solve_sim..|].
  { rewrite lookup_insert. done. }
Hai Dang's avatar
Hai Dang committed
110 111
  apply: sim_body_result=>_/=.
  apply: sim_body_let_r=>/=. (* FIXME: figure out why [sim_apply_r] does the wrong thing here *)
Ralf Jung's avatar
Ralf Jung committed
112
  (* We can go back to simple mode! *)
Ralf Jung's avatar
Ralf Jung committed
113
  eapply (sim_simplify (fun_post_simple c)). { by eauto. }
114
  simplify_eq/=. clear- AREL FREL LOOK.
115
  (* Call unknown function "g" *)
Ralf Jung's avatar
Ralf Jung committed
116 117 118 119
  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
120
  (* ## Step (3) in the proof sketch:
121
    With similar reasoning to Step (2), "g" must not have accessed "x". *)
Ralf Jung's avatar
Ralf Jung committed
122
  (* Copy local (left). We drop to complex just because simple does not support this yet. *)
123
  intros σs σt.
Ralf Jung's avatar
Ralf Jung committed
124
  sim_apply_l sim_body_copy_local_l; [solve_sim..|].
Hai Dang's avatar
Hai Dang committed
125
  apply: sim_body_result=>_/=.
Ralf Jung's avatar
Ralf Jung committed
126
  (* Copy unique (left) *)
Hai Dang's avatar
Hai Dang committed
127
  sim_apply_l sim_body_deref_l=>/=.
Ralf Jung's avatar
Ralf Jung committed
128 129
  sim_apply_l sim_body_copy_unique_l; [try solve_sim..|].
  { rewrite lookup_insert. done. }
Hai Dang's avatar
Hai Dang committed
130 131
  apply: sim_body_result=>Hval/=.
  apply: sim_body_let_l=>/=.
Ralf Jung's avatar
Ralf Jung committed
132 133
  (* Free stuff *)
  eapply (sim_simplify (fun_post_simple c)). { by eauto. }
Ralf Jung's avatar
Ralf Jung committed
134
  sim_apply sim_simple_free_local_1; [solve_sim..|]. simpl.
Ralf Jung's avatar
Ralf Jung committed
135
  sim_apply sim_simple_let=>/=.
Ralf Jung's avatar
Ralf Jung committed
136
  (* Finishing up. *)
Ralf Jung's avatar
Ralf Jung committed
137
  apply: sim_simple_result. split.
138
  - solve_res.
Ralf Jung's avatar
Ralf Jung committed
139
  - constructor; simpl; auto.
Hai Dang's avatar
Hai Dang committed
140
Qed.
Ralf Jung's avatar
Ralf Jung committed
141

Ralf Jung's avatar
Ralf Jung committed
142 143
(** Top-level theorem: Two programs that only differ in the
"ex1" function are related. *)
Ralf Jung's avatar
Ralf Jung committed
144
Corollary ex1 (prog: fn_env) :
Ralf Jung's avatar
Ralf Jung committed
145
  stuck_decidable 
Ralf Jung's avatar
Ralf Jung committed
146
  prog_wf prog 
Ralf Jung's avatar
Ralf Jung committed
147
  let prog_src := <["ex1":=ex1_unopt]> prog in
Ralf Jung's avatar
Ralf Jung committed
148 149 150
  let prog_tgt := <["ex1":=ex1_opt]> prog in
  behave_prog prog_tgt <1= behave_prog prog_src.
Proof.
151 152 153 154
  intros Hdec Hwf.
  (* To show behavior inclusion, we show that the programs are in the program
    simulation relation. *)
  apply sim_prog_sim_classical.
Ralf Jung's avatar
Ralf Jung committed
155
  { apply Hdec. }
Ralf Jung's avatar
Ralf Jung committed
156
  { apply has_main_insert, Hwf; done. }
157 158
  (* Program simulation means that every function in one program simulates the
    function in the other program with the same function id. *)
Ralf Jung's avatar
Ralf Jung committed
159 160
  apply sim_mod_funs_local.
  apply sim_mod_funs_insert; first done.
161 162 163 164 165
  - (* the unopt version can simulate the opt version of ex1. *)
    exact: ex1_sim_fun.
  - (* for other functions, they simulate themselves. That is, the simulation
      relation is reflexive. *)
    exact: sim_mod_funs_refl.
Ralf Jung's avatar
Ralf Jung committed
166
Qed.
Ralf Jung's avatar
Ralf Jung committed
167 168

Print Assumptions ex1.