ex3.v 1.09 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
From stbor.sim Require Import local invariant refl_step.
2 3 4

Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
5 6
(** Moving a write to a mutable reference up across unknown code. *)

Hai Dang's avatar
Hai Dang committed
7
(* TODO: check if Free is in the right place *)
Hai Dang's avatar
Hai Dang committed
8
(* Assuming x : &mut i32 *)
Ralf Jung's avatar
Ralf Jung committed
9
Definition ex3 : function :=
Hai Dang's avatar
Hai Dang committed
10
  fun: ["i"],
Ralf Jung's avatar
Ralf Jung committed
11
    let: "x" := new_place (&mut int) "i" in
Hai Dang's avatar
Hai Dang committed
12
    retag_place "x" (RefPtr Mutable) int FnEntry ;;
Hai Dang's avatar
Hai Dang committed
13
    *{int} "x" <- #[42] ;;
Ralf Jung's avatar
Ralf Jung committed
14 15
    let: "v" := Call #[ScFnPtr "f"] [] in
    *{int} "x" <- #[13] ;;
Hai Dang's avatar
Hai Dang committed
16
    Free "x" ;;
Ralf Jung's avatar
Ralf Jung committed
17
    "v"
18 19
  .

Ralf Jung's avatar
Ralf Jung committed
20
Definition ex3_opt_1 : function :=
Hai Dang's avatar
Hai Dang committed
21
  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
    retag_place "x" (RefPtr Mutable) int FnEntry ;;
Hai Dang's avatar
Hai Dang committed
24
    *{int} "x" <- #[42] ;;
Ralf Jung's avatar
Ralf Jung committed
25
    *{int} "x" <- #[13] ;;
Hai Dang's avatar
Hai Dang committed
26 27 28
    let: "v" := Call #[ScFnPtr "f"] [] in
    Free "x" ;;
    "v"
29 30
  .

Ralf Jung's avatar
Ralf Jung committed
31
Definition ex3_opt_2 : function :=
Hai Dang's avatar
Hai Dang committed
32
  fun: ["i"],
Ralf Jung's avatar
Ralf Jung committed
33
    let: "x" := new_place (&mut int) "i" in
Hai Dang's avatar
Hai Dang committed
34
    retag_place "x" (RefPtr Mutable) int FnEntry ;;
Ralf Jung's avatar
Ralf Jung committed
35
    *{int} "x" <- #[13] ;;
Hai Dang's avatar
Hai Dang committed
36 37 38
    let: "v" := Call #[ScFnPtr "f"] [] in
    Free "x" ;;
    "v"
39 40
  .

Hai Dang's avatar
Hai Dang committed
41
(* TODO: show refinement to be transitive *)
Ralf Jung's avatar
Ralf Jung committed
42
Lemma ex3_sim_fun : ⊨ᶠ ex3  ex3_opt_1.
43
Proof.
Ralf Jung's avatar
Ralf Jung committed
44
Abort.