ex1.v 715 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
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

Set Default Proof Using "Type".

(* Assuming x : &mut i32 *)
Definition ex1 : expr :=
  let: "x" := new_place (&mut int) &"i" in
  Retag "x" Default ;;
  Call #[ScFnPtr "f"] [] ;;
  *{int} "x" <- #[42] ;;
  Call #[ScFnPtr "g"] [] ;;
  Copy *{int} "x"
  .

Definition ex1_opt : expr :=
  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"
  .

Lemma ex1_sim_body fs ft r n σs σt :
  (* TODO: what's in r? *)
  r {n, fs,ft} (ex1, σs)  (ex1_opt, σt) : (λ r' _ vs' σs' vt' σt', vrel_expr r' vs' vt').
Proof.
Abort.