ex1.v 668 Bytes
Newer Older
Hai Dang's avatar
Hai Dang committed
1
From stbor.sim Require Import local invariant refl_step.
Hai Dang's avatar
Hai Dang committed
2
3
4
5

Set Default Proof Using "Type".

(* Assuming x : &mut i32 *)
Hai Dang's avatar
Hai Dang committed
6
7
8
9
10
11
12
13
Definition ex1 : function :=
  fun: ["i"],
    let: "x" := new_place (&mut int) &"i" in
    Retag "x" Default ;;
    Call #[ScFnPtr "f"] [] ;;
    *{int} "x" <- #[42] ;;
    Call #[ScFnPtr "g"] [] ;;
    Copy *{int} "x"
Hai Dang's avatar
Hai Dang committed
14
15
  .

Hai Dang's avatar
Hai Dang committed
16
17
18
19
20
21
22
23
24
Definition ex1_opt : function :=
  fun: ["i"],
    let: "x" := new_place (&mut int) &"i" in
    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
25
26
  .

Hai Dang's avatar
Hai Dang committed
27
Lemma ex1_sim_body fs ft : {fs,ft} ex1 ≥ᶠ ex1_opt.
Hai Dang's avatar
Hai Dang committed
28
29
Proof.
Abort.