update and fix examples

_CoqProject

 -Q theories stbor
 -arg -w -arg -notation-overridden,-projection-no-head-constant,-redundant-canonical-projection
+
 theories/lang/helpers.v
 theories/lang/type.v
 theories/lang/lang_base.v
@@ -15,6 +16,7 @@ theories/lang/steps_progress.v
 theories/lang/steps_inversion.v
 theories/lang/steps_retag.v
 theories/lang/examples.v
+
 theories/sim/behavior.v
 theories/sim/global.v
 theories/sim/global_adequacy.v
@@ -29,7 +31,10 @@ theories/sim/body.v
 theories/sim/refl_step.v
 theories/sim/left_step.v
 theories/sim/right_step.v
+
 theories/opt/ex1.v
-theories/opt/ex1_2.v
+theories/opt/ex1_down.v
 theories/opt/ex2.v
-theories/opt/ex2_2.v
+theories/opt/ex2_down.v
+theories/opt/ex3.v
+theories/opt/ex3_down.v

theories/opt/ex1.v

@@ -2,10 +2,12 @@ From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 
+(** Moving read of mutable reference up across code not using that ref. *)
+
 (* Assuming x : &mut i32 *)
 Definition ex1 : function :=
   fun: ["i"],
-    let: "x" := new_place (&mut int) &"i" in
+    let: "x" := new_place (&mut int) "i" in (* put argument into place *)
     Retag "x" Default ;;
     Call #[ScFnPtr "f"] [] ;;
     *{int} "x" <- #[42] ;;
@@ -15,7 +17,7 @@ Definition ex1 : function :=
 
 Definition ex1_opt : function :=
   fun: ["i"],
-    let: "x" := new_place (&mut int) &"i" in
+    let: "x" := new_place (&mut int) "i" in
     Retag "x" Default ;;
     Call #[ScFnPtr "f"] [] ;;
     *{int} "x" <- #[42] ;;

theories/opt/ex1_down.v

+From stbor.sim Require Import local invariant refl_step.
+
+Set Default Proof Using "Type".
+
+(** Moving a read of a mutable reference down across code that *may* use that ref. *)
+
+(* Assuming x : &mut i32 *)
+Definition ex1_down : function :=
+  fun: ["i"],
+    let: "x" := new_place (&mut int) "i" in (* put argument into place *)
+    Retag "x"  FnEntry ;;
+    let: "v" := Copy *{int} "x" in
+    Call #[ScFnPtr "f"] [] ;;
+    "v"
+    .
+
+Definition ex1_down_opt : function :=
+  fun: ["i"],
+    let: "x" := new_place (&mut int) "i" in
+    Retag "x"  FnEntry ;;
+    Call #[ScFnPtr "f"] [] ;;
+    Copy *{int} "x"
+    .
+
+
+Lemma ex1_down_sim_fun fs ft : ⊨{fs,ft} ex1_down ≥ᶠ ex1_down_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.

theories/opt/ex2.v

@@ -2,10 +2,12 @@ From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 
+(** Moving read of shared ref up across code that *may* use that ref. *)
+
 (* Assuming x : & i32 *)
 Definition ex2 : function :=
   fun: ["i"],
-    let: "x" := new_place (& int) &"i" in
+    let: "x" := new_place (& int) "i" in
     Retag "x" Default ;;
     Copy *{int} "x" ;;
     Call #[ScFnPtr "f"] ["x"] ;;
@@ -14,7 +16,7 @@ Definition ex2 : function :=
 
 Definition ex2_opt : function :=
   fun: ["i"],
-    let: "x" := new_place (& int) &"i" in
+    let: "x" := new_place (& int) "i" in
     Retag "x" Default ;;
     Copy *{int} "x" ;;
     let: "v" := Copy *{int} "x" in

theories/opt/ex2_2.v → theories/opt/ex2_down.v

@@ -2,26 +2,28 @@ From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 
+(** Moving a read of a shared reference down across code that *may* use that ref. *)
+
 (* Assuming x : & i32 *)
-Definition ex2_2 : function :=
+Definition ex2_down : function :=
   fun: ["i"],
-    let: "x" := new_place (& int) &"i" in
+    let: "x" := new_place (& int) "i" in
     Retag "x"  FnEntry ;;
     let: "v" := Copy *{int} "x" in
     Call #[ScFnPtr "f"] ["x"] ;;
     "v"
     .
 
-Definition ex2_2_opt : function :=
+Definition ex2_down_opt : function :=
   fun: ["i"],
-    let: "x" := new_place (& int) &"i" in
+    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.
+Lemma ex2_down_sim_fun fs ft : ⊨{fs,ft} ex2_down ≥ᶠ ex2_down_opt.
 Proof.
   intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
   destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.

theories/opt/ex1_2.v → theories/opt/ex3.v

@@ -2,34 +2,37 @@ From stbor.sim Require Import local invariant refl_step.
 
 Set Default Proof Using "Type".
 
+(** Moving a write to a mutable reference up across unknown code. *)
+
 (* Assuming x : &mut i32 *)
-Definition ex1_2 : function :=
+Definition ex3 : function :=
   fun: ["i"],
-    let: "x" := new_place (&mut int) &"i" in
+    let: "x" := new_place (&mut int) "i" in
     Retag "x"  FnEntry ;;
     *{int} "x" <- #[42] ;;
-    Call #[ScFnPtr "f"] [] ;;
-    *{int} "x" <- #[13]
+    let: "v" := Call #[ScFnPtr "f"] [] in
+    *{int} "x" <- #[13] ;;
+    "v"
   .
 
-Definition ex1_2_opt_1 : function :=
+Definition ex3_opt_1 : function :=
   fun: ["i"],
-    let: "x" := new_place (&mut int) &"i" in
+    let: "x" := new_place (&mut int) "i" in
     Retag "x"  FnEntry ;;
-    Call #[ScFnPtr "f"] [] ;;
     *{int} "x" <- #[42] ;;
-    *{int} "x" <- #[13]
+    *{int} "x" <- #[13] ;;
+    Call #[ScFnPtr "f"] []
   .
 
-Definition ex1_2_opt_2 : function :=
+Definition ex3_opt_2 : function :=
   fun: ["i"],
-    let: "x" := new_place (&mut int) &"i" in
+    let: "x" := new_place (&mut int) "i" in
     Retag "x"  FnEntry ;;
-    Call #[ScFnPtr "f"] [] ;;
-    *{int} "x" <- #[13]
+    *{int} "x" <- #[13] ;;
+    Call #[ScFnPtr "f"] []
   .
 
-Lemma ex1_2_sim_fun fs ft : ⊨{fs,ft} ex1_2 ≥ᶠ ex1_2_opt_1.
+Lemma ex3_sim_fun fs ft : ⊨{fs,ft} ex3 ≥ᶠ ex3_opt_1.
 Proof.
   intros r es et els elt σs σt FAs FAt FREL SUBSTs SUBSTt.
   destruct els as [|efs []]; [done| |done].  simpl in SUBSTs.
@@ -38,4 +41,4 @@ Proof.
   (* InitCall *)
   exists 10%nat.
   apply sim_body_init_call. simpl.
-Abort.
\ No newline at end of file
+Abort.

theories/opt/ex3_down.v

+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 *)
+Definition ex3_down : function :=
+  fun: ["i"],
+    let: "x" := new_place (&mut int) "i" in
+    Retag "x"  FnEntry ;;
+    *{int} "x" <- #[42] ;;
+    let: "v" := Call #[ScFnPtr "f"] [] in
+    *{int} "x" <- #[13] ;;
+    "v"
+  .
+
+Definition ex3_down_opt_1 : function :=
+  fun: ["i"],
+    let: "x" := new_place (&mut int) "i" in
+    Retag "x"  FnEntry ;;
+    let: "v" := Call #[ScFnPtr "f"] [] in
+    *{int} "x" <- #[42] ;;
+    *{int} "x" <- #[13] ;;
+    "v"
+  .
+
+Definition ex3_down_opt_2 : function :=
+  fun: ["i"],
+    let: "x" := new_place (&mut int) "i" in
+    Retag "x"  FnEntry ;;
+    let: "v" := Call #[ScFnPtr "f"] [] in
+    *{int} "x" <- #[13] ;;
+    "v"
+  .
+
+Lemma ex3_down_sim_fun fs ft : ⊨{fs,ft} ex3_down ≥ᶠ ex3_down_opt_1.
+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.