add opt examples

_CoqProject

@@ -22,6 +22,7 @@ theories/sim/local_adequacy.v
 theories/sim/program.v
 theories/sim/sflib.v
 theories/sim/one_step.v
-theories/opt/foo.v
+theories/opt/ex1.v
 theories/opt/ex1_2.v
+theories/opt/ex2.v
 theories/opt/ex2_2.v

theories/lang/notation.v

@@ -40,7 +40,6 @@ Notation "# v" := (Val v%V%R%L) (at level 8, format "# v") : expr_scope.
 
 (** Some common types *)
 Notation int := (FixedSize 1).
-Notation int_arr n := (FixedSize n).
 Notation "'&mut' T" := (Reference (RefPtr Mutable) T%T)
   (at level 8, format "&mut  T") : lrust_type.
 Notation "'&' T" := (Reference (RefPtr Immutable) T%T)

theories/opt/ex1.v

+From stbor.sim Require Import local invariant one_step.
+
+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.

theories/opt/ex1_2.v

@@ -2,36 +2,40 @@ From stbor.sim Require Import local invariant one_step.
 
 Set Default Proof Using "Type".
 
+(* Assuming x : &mut i32 *)
 Definition ex1_2 : function :=
-  fun: ["x"],
+  fun: ["i"],
+  let: "x" := new_place (&mut int) &"i" in
   Retag "x"  FnEntry ;;
-  *{int} (Copy1 "x") <- #[42] ;;
+  *{int} "x" <- #[42] ;;
   Call #[ScFnPtr "f"] [] ;;
-  *{int} (Copy1 "x") <- #[13]
+  *{int} "x" <- #[13]
   .
 
 Definition ex1_2_opt_1 : function :=
-  fun: ["x"],
+  fun: ["i"],
+  let: "x" := new_place (&mut int) &"i" in
   Retag "x"  FnEntry ;;
   Call #[ScFnPtr "f"] [] ;;
-  *{int} (Copy1 "x") <- #[42] ;;
-  *{int} (Copy1 "x") <- #[13]
+  *{int} "x" <- #[42] ;;
+  *{int} "x" <- #[13]
   .
 
 Definition ex1_2_opt_2 : function :=
-  fun: ["x"],
+  fun: ["i"],
+  let: "x" := new_place (&mut int) &"i" in
   Retag "x"  FnEntry ;;
   Call #[ScFnPtr "f"] [] ;;
-  *{int} (Copy1 "x") <- #[13]
+  *{int} "x" <- #[13]
   .
 
 Lemma ex1_2_sim_fun fs ft : ⊨{fs,ft} ex1_2 ≥ᶠ ex1_2_opt_1.
 Proof.
-  intros [r1 r2] es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
+  intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
   destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
   destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
 
   (* InitCall *)
-  exists 1%nat.
-  apply sim_body_init_call. rewrite pair_op.
+  exists 10%nat.
+  apply sim_body_init_call. simpl.
 Abort.
\ No newline at end of file

theories/opt/ex2.v

+From stbor.sim Require Import local invariant one_step.
+
+Set Default Proof Using "Type".
+
+(* Assuming x : & i32 *)
+Definition ex2 : expr :=
+  let: "x" := new_place (& int) &"i" in
+  Retag "x" Default ;;
+  Copy *{int} "x" ;;
+  Call #[ScFnPtr "f"] ["x"] ;;
+  Copy *{int} "x"
+  .
+
+Definition ex2_opt : expr :=
+  let: "x" := new_place (& int) &"i" in
+  Retag "x" Default ;;
+  Copy *{int} "x" ;;
+  let: "v" := Copy *{int} "x" in
+  Call #[ScFnPtr "f"] ["x"] ;;
+  "v"
+  .
+
+Lemma ex2_sim_body fs ft r n σs σt :
+  (* TODO: what's in r? *)
+  r ⊨{n, fs,ft} (ex2, σs) ≥ (ex2_opt, σt) : (λ r' _ vs' σs' vt' σt', vrel_expr r' vs' vt').
+Proof.
+Abort.

theories/opt/ex2_2.v

@@ -2,8 +2,10 @@ From stbor.sim Require Import local invariant one_step.
 
 Set Default Proof Using "Type".
 
+(* Assuming x : & i32 *)
 Definition ex2_2 : function :=
-  fun: ["x"],
+  fun: ["i"],
+    let: "x" := new_place (& int) &"i" in
     Retag "x"  FnEntry ;;
     let: "v" := Copy *{int} "x" in
     Call #[ScFnPtr "f"] ["x"] ;;
@@ -11,8 +13,21 @@ Definition ex2_2 : function :=
     .
 
 Definition ex2_2_opt : function :=
-  fun: ["x"],
+  fun: ["i"],
+    let: "x" := new_place (& int) &"i" in
     Retag "x"  FnEntry ;;
     Call #[ScFnPtr "f"] ["x"] ;;
     Copy *{int} "x"
     .
+
+
+Lemma ex2_2_sim_fun fs ft : ⊨{fs,ft} ex2_2 ≥ᶠ ex2_2_opt.
+Proof.
+  intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
+  destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
+  destruct elt as [|eft []]; [done| |done].  simpl in SUBSTt. simplify_eq.
+
+  (* InitCall *)
+  exists 10%nat.
+  apply sim_body_init_call. simpl.
+Abort.