ex1.v 2.24 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From stbor.sim Require Import local invariant refl tactics simple program.
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 *)
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_place=>/=.
39
  (* Write *)
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; [done|solve_res|].
Ralf Jung's avatar
Ralf Jung committed
42
  intros arg ->. simpl.
43
44
  sim_apply sim_simple_let_val=>/=.
  apply sim_simple_place.
Ralf Jung's avatar
Ralf Jung committed
45
46
  (* Retag. *)
  sim_apply sim_simple_let_place=>/=.
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.
50
  sim_apply sim_simple_retag_local; [solve_res|done|solve_res|].
Ralf Jung's avatar
Ralf Jung committed
51
52
53
  move=>l_i tg_i hplt /= Hl_i.
  (* Call *)
  sim_apply sim_simple_let_val=>/=.
54
  sim_apply (sim_simple_call 10 [] [] ε); [done|done|solve_res|].
Ralf Jung's avatar
Ralf Jung committed
55
56
57
  intros rf frs frt FREL.
  apply sim_simple_val.

Ralf Jung's avatar
Ralf Jung committed
58
59
Admitted.

Ralf Jung's avatar
Ralf Jung committed
60
61
(** Top-level theorem: Two programs that only differ in the
"ex1" function are related. *)
Ralf Jung's avatar
Ralf Jung committed
62
Corollary ex1 (prog: fn_env) :
Ralf Jung's avatar
Ralf Jung committed
63
64
  stuck_decidable 
  has_main prog 
Ralf Jung's avatar
Ralf Jung committed
65
  let prog_src := <["ex1":=ex1_unopt]> prog in
Ralf Jung's avatar
Ralf Jung committed
66
67
68
69
70
71
  let prog_tgt := <["ex1":=ex1_opt]> prog in
  behave_prog prog_tgt <1= behave_prog prog_src.
Proof.
  intros Hdec Hmain. apply sim_prog_sim_classical.
  { apply Hdec. }
  { apply has_main_insert; done. }
Ralf Jung's avatar
Ralf Jung committed
72
73
  apply sim_mod_funs_local.
  apply sim_mod_funs_insert; first done.
Ralf Jung's avatar
Ralf Jung committed
74
  - exact: ex1_sim_body.
Ralf Jung's avatar
Ralf Jung committed
75
76
  - exact: sim_mod_funs_refl.
Qed.
Ralf Jung's avatar
Ralf Jung committed
77
78

Print Assumptions ex1.