ex3_down.v 1.05 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6 7
From stbor.sim Require Import local invariant refl_step.

Set Default Proof Using "Type".

(** Moving a write to a mutable reference down across unknown code. *)

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

Definition ex3_down_opt_1 : function :=
  fun: ["i"],
    let: "x" := new_place (&mut int) "i" in
Hai Dang's avatar
Hai Dang committed
22
    retag_place "x" (RefPtr Mutable) int FnEntry ;;
Ralf Jung's avatar
Ralf Jung committed
23 24 25
    let: "v" := Call #[ScFnPtr "f"] [] in
    *{int} "x" <- #[42] ;;
    *{int} "x" <- #[13] ;;
Hai Dang's avatar
Hai Dang committed
26
    Free "x" ;;
Ralf Jung's avatar
Ralf Jung committed
27 28 29 30 31 32
    "v"
  .

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

Hai Dang's avatar
Hai Dang committed
40
Lemma ex3_down_sim_fun : ⊨ᶠ ex3_down_unopt  ex3_down_opt_1.
Ralf Jung's avatar
Ralf Jung committed
41 42
Proof.
Abort.