add some asymmetric rules

theories/lang/steps_retag.v

@@ -2,6 +2,11 @@ From stbor.lang Require Export defs steps_foreach steps_list.
 
 Set Default Proof Using "Type".
 
+Definition tag_in t (stk: stack) :=
+  ∃ pm opro, pm ≠ Disabled ∧ mkItem pm (Tagged t) opro ∈ stk.
+Definition tag_in_stack σ l t :=
+  ∃ stk, σ.(sst) !! l = Some stk ∧ tag_in t stk.
+
 (** Active protector preserving *)
 Definition active_preserving (cids: call_id_stack) (stk stk': stack) :=
   ∀ pm t c, c ∈ cids → mkItem pm t (Some c) ∈ stk → mkItem pm t (Some c) ∈ stk'.
@@ -536,3 +541,36 @@ Proof.
   rewrite -{1}(take_drop n stk) in ND. intros ?.
   eapply (remove_check_incompatible_items _ _ _ _ idx it i ti ND); eauto.
 Qed.
+
+(* Property of [t] that when used to access [stk], it will not change [stk] *)
+Definition stack_preserving_tag
+  (stk: stack) (t: ptr_id) (k: access_kind) : Prop :=
+  ∃ n pm, find_granting stk k (Tagged t) = Some (n, pm) ∧
+    match k with
+    | AccessRead => ∀ it, it ∈ take n stk → it.(perm) ≠ Unique
+    | AccessWrite => find_first_write_incompatible (take n stk) pm = Some O
+    end.
+
+Lemma stack_preserving_tag_elim stk t kind :
+  stack_preserving_tag stk t kind →
+  ∀ cids, ∃ n stk',
+  access1 stk kind (Tagged t) cids = Some (n, stk') ∧ stk' = stk.
+Proof.
+Abort.
+
+Lemma stack_preserving_tag_intro stk kind t cids n stk' :
+  access1 stk kind (Tagged t) cids = Some (n, stk') →
+  stack_preserving_tag stk' t kind.
+Proof.
+Abort.
+
+Lemma stack_preserving_tag_unique_head stk t opro kind :
+  is_stack_head (mkItem Unique (Tagged t) opro) stk →
+  stack_preserving_tag stk t kind.
+Proof.
+Abort.
+
+Lemma stack_preserving_tag_active_SRO stk t :
+  t ∈ active_SRO stk → stack_preserving_tag stk t AccessRead.
+Proof.
+Abort.

theories/opt/ex1.v

@@ -3,27 +3,27 @@ From stbor.sim Require Import local invariant refl_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 : 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"
   .
 
-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"
+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"
   .
 
-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').
+Lemma ex1_sim_body fs ft : ⊨{fs,ft} ex1 ≥ᶠ ex1_opt.
 Proof.
 Abort.

theories/opt/ex1_2.v

@@ -5,28 +5,28 @@ Set Default Proof Using "Type".
 (* Assuming x : &mut i32 *)
 Definition ex1_2 : function :=
   fun: ["i"],
-  let: "x" := new_place (&mut int) &"i" in
-  Retag "x"  FnEntry ;;
-  *{int} "x" <- #[42] ;;
-  Call #[ScFnPtr "f"] [] ;;
-  *{int} "x" <- #[13]
+    let: "x" := new_place (&mut int) &"i" in
+    Retag "x"  FnEntry ;;
+    *{int} "x" <- #[42] ;;
+    Call #[ScFnPtr "f"] [] ;;
+    *{int} "x" <- #[13]
   .
 
 Definition ex1_2_opt_1 : function :=
   fun: ["i"],
-  let: "x" := new_place (&mut int) &"i" in
-  Retag "x"  FnEntry ;;
-  Call #[ScFnPtr "f"] [] ;;
-  *{int} "x" <- #[42] ;;
-  *{int} "x" <- #[13]
+    let: "x" := new_place (&mut int) &"i" in
+    Retag "x"  FnEntry ;;
+    Call #[ScFnPtr "f"] [] ;;
+    *{int} "x" <- #[42] ;;
+    *{int} "x" <- #[13]
   .
 
 Definition ex1_2_opt_2 : function :=
   fun: ["i"],
-  let: "x" := new_place (&mut int) &"i" in
-  Retag "x"  FnEntry ;;
-  Call #[ScFnPtr "f"] [] ;;
-  *{int} "x" <- #[13]
+    let: "x" := new_place (&mut int) &"i" in
+    Retag "x"  FnEntry ;;
+    Call #[ScFnPtr "f"] [] ;;
+    *{int} "x" <- #[13]
   .
 
 Lemma ex1_2_sim_fun fs ft : ⊨{fs,ft} ex1_2 ≥ᶠ ex1_2_opt_1.

theories/opt/ex2.v

@@ -3,25 +3,25 @@ From stbor.sim Require Import local invariant refl_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 : function :=
+  fun: ["i"],
+    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"
+Definition ex2_opt : function :=
+  fun: ["i"],
+    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').
+Lemma ex2_sim_body fs ft : ⊨{fs,ft} ex2 ≥ᶠ ex2_opt.
 Proof.
 Abort.

theories/sim/left_step.v

+From iris.algebra Require Import local_updates.
+
+From stbor.lang Require Import steps_progress steps_inversion steps_retag.
+From stbor.sim Require Export instance.
+
+Set Default Proof Using "Type".
+
+Lemma sim_body_copy_left_1
+  fs ft (r: resUR) k (h: heapletR) n l t et σs σt Φ
+  (UNIQUE: r.1 !! t ≡ Some (k, h))
+  (InD: l ∈ dom (gset loc) h) :
+  (∀ s, σs.(shp) !! l = Some s → r ⊨{n,fs,ft} (#[s%S], σs) ≥ (et, σt) : Φ : Prop) →
+  r ⊨{n,fs,ft} (Copy (Place l (Tagged t) int), σs) ≥ (et, σt) : Φ.
+Proof.
+  intros COND. pfold. intros NT r_f WSAT.
+  edestruct NT as [[]|[es1 [σs1 STEP1]]]; [constructor 1|done|].
+  destruct (tstep_copy_inv _ _ _ _ _ _ _ STEP1) as (vs & α' & ? & Eqvs & READ & ?).
+  subst es1 σs1. rewrite /= read_mem_equation_1 /= in Eqvs.
+  destruct (σs.(shp) !! l) as [s|] eqn:Eqs; [|done]. simpl in Eqvs. simplify_eq.
+  specialize (COND _ eq_refl).
+
+  (* we need to invoke WSAT to know that α' = σs.(sst) *)
+  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
+
+  (* once we know that the state did not change, we can use COND. *)
+  have NT2 := never_stuck_tstep_once _ _ _ _ _ STEP1 NT.
+  punfold COND.
+
+  split.
+  { (* this comes from COND *) admit. }
+  { (* follows COND *) admit. }
+  { (* follows COND *) admit. }
+Abort.

theories/sim/local_adequacy.v

@@ -2,7 +2,8 @@ From Coq Require Import Program.Equality Lia.
 From Paco Require Import paco.
 
 From stbor.lang Require Import steps_wf steps_inversion.
-From stbor.sim Require Import behavior global local invariant sflib global_adequacy one_step.
+From stbor.sim Require Import sflib behavior global local.
+From stbor.sim Require Import invariant global_adequacy refl_step.
 
 Set Default Proof Using "Type".
 

theories/sim/right_step.v

+From iris.algebra Require Import local_updates.
+
+From stbor.lang Require Import steps_progress steps_inversion steps_retag.
+From stbor.sim Require Export instance.
+
+Set Default Proof Using "Type".
+
+Lemma sim_body_copy_right_1
+  fs ft (r: resUR) k (h: heapletR) n l t s es σs σt Φ
+  (* we know we're going to read s *)
+  (UNIQUE: r.1 !! t ≡ Some (k, h))
+  (InD: h !! l ≡ Some (to_agree s))
+  (IN: tag_in_stack σt l t) :
+  (σt.(shp) !! l = Some s → r ⊨{n,fs,ft} (es, σs) ≥ (#[s%S], σt) : Φ : Prop) →
+  r ⊨{n,fs,ft} (es, σs) ≥ (Copy (Place l (Tagged t) int), σt) : Φ.
+Proof.
+Abort.