diff --git a/_CoqProject b/_CoqProject
index d01a2f3..b74b689 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,6 +3,7 @@
 src/guarding/internal/auth_frag_util.v
 src/guarding/internal/wsat_util.v
 src/guarding/internal/factoring_upred.v
+src/guarding/internal/inved.v
 
 src/guarding/own_and.v
 src/guarding/own_and_own_sep.v
@@ -11,9 +12,7 @@ src/guarding/guard.v
 src/guarding/tactics.v
 src/guarding/guard_later_pers.v
 
-src/guarding/storage_protocol/inved.v
 src/guarding/storage_protocol/protocol.v
-src/guarding/storage_protocol/protocol_relational.v
 src/guarding/storage_protocol/base_storage_opt.v
 
 src/guarding/lib/lifetime.v
diff --git a/src/examples/counting.v b/src/examples/counting.v
index 3035a36..0b119ed 100644
--- a/src/examples/counting.v
+++ b/src/examples/counting.v
@@ -1,5 +1,4 @@
 From iris.base_logic.lib Require Import invariants.
-From lang Require Import lang simp adequacy primitive_laws.
 
 From iris.base_logic Require Export base_logic.
 From iris.program_logic Require Export weakestpre.
@@ -10,22 +9,15 @@ From iris.proofmode Require Import reduction.
 From iris.proofmode Require Import ltac_tactics.
 From iris.proofmode Require Import class_instances.
 From iris.program_logic Require Import ectx_lifting.
-From lang Require Import notation tactics class_instances.
-From lang Require Import heap_ra.
-From lang Require Import lang.
-From iris Require Import options.
 From iris.algebra Require Import auth.
 
 Require Import guarding.guard.
-
 Require Import guarding.storage_protocol.protocol.
-Require Import guarding.storage_protocol.inved.
 
 Require Import examples.misc_tactics.
 
-
 Context {Σ: gFunctors}.
-Context `{!simpGS Σ}.
+Context `{!invGS Σ}.
 
 Definition COUNT_NAMESPACE := nroot .@ "count".
 
@@ -57,7 +49,7 @@ Proof. split.
   - unfold Transitive, equiv, co_equiv. intros x y z a b. subst x. trivial.
 Qed.
 
-Global Instance co_inv : PInv Co := λ t , match t with
+Global Instance co_inv : SPInv Co := λ t , match t with
   | Refs n => n = 0
   | Counters count counters => count = 0
 end.
@@ -82,45 +74,33 @@ Proof.
   - unfold Comm. intros; unfold "⋅", nat_op_instance, "≡", nat_equiv_instance. lia.*)
 Qed.
 
-Definition count_protocol_mixin : @ProtocolMixin Co 
-      co_equiv co_pcore co_op co_valid _ _ _.
-Proof. split.
-  - exact count_ra_mixin.
-  - unfold LeftId. intros x. unfold ε, co_unit, "⋅", co_op, "≡", co_equiv. destruct x; trivial.
-      f_equal. lia.
-  - intros p X. unfold "✓", co_valid. destruct p; trivial.
-  - unfold Proper, "==>", impl. intros x y X. unfold "≡", co_equiv in X.
-      subst x. trivial.
-Qed.
-  
-Local Instance co_interp_instance : Interp Co nat := λ co , 
+Local Instance co_interp_instance : SPInterp Co nat := λ co , 
   match co with
   | Refs _ => 0%nat
   | Counters _ c => c + 1
   end.
 
-Definition count_storage_mixin : @StorageMixin Co nat
-    co_equiv co_pcore co_op co_valid _ _ _ _ _ _ _ _ _.
+Local Instance count_storage_mixin_ii : StorageMixinII Co nat.
 Proof. split.
-  - exact count_protocol_mixin.
-  - apply nat_ra_mixin.
+  - exact count_ra_mixin.
+  - exact nat_ra_mixin.
+  - unfold LeftId. intros x. unfold ε, co_unit, "⋅", co_op, "≡", co_equiv. destruct x; trivial.
+      f_equal. lia.
   - unfold LeftId. intros x. unfold ε, nat_unit_instance, "⋅", nat_op_instance. trivial.
-  - unfold Proper, "==>". intros. unfold "≡", co_equiv in H. destruct x, y; trivial; try contradiction; try discriminate.
-    inversion H. trivial.
+  - unfold Proper, "==>". intros x y Heq. unfold sp_inv, co_inv. destruct x, y; trivial;
+      try contradiction; try discriminate; inversion Heq; trivial.
+  - unfold Proper, "==>". intros x y Heq. unfold "≡", co_equiv in Heq. destruct x, y; trivial; try contradiction; try discriminate; inversion Heq; trivial.
   - intros. unfold "✓", nat_valid_instance. trivial.
 Qed.
 
 Class co_logicG Σ :=
     {
-      co_logic_inG : inG Σ 
-        (authUR (inved_protocolUR (protocol_mixin Co (nat) (count_storage_mixin))))
+      #[local] count_sp_inG ::
+        sp_logicG (storage_mixin_from_ii count_storage_mixin_ii) Σ
     }.
-Local Existing Instance co_logic_inG.
-
 
 Definition co_logicΣ : gFunctors := #[
-  GFunctor
-        (authUR (inved_protocolUR (protocol_mixin Co (nat) (count_storage_mixin))))
+  sp_logicΣ (storage_mixin_from_ii count_storage_mixin_ii)
 ].
 
 Global Instance subG_co_logicΣ {Σ} : subG co_logicΣ Σ → co_logicG Σ.
@@ -129,7 +109,7 @@ Proof. solve_inG. Qed.
 Section Counting.
 
 Context {Σ: gFunctors}.
-Context `{@co_logicG Σ}.
+Context `{co_in_Σ: !@co_logicG Σ}.
 Context `{!invGS Σ}.
 
 Fixpoint sep_pow (n: nat) (P: iProp Σ) : iProp Σ :=
@@ -141,7 +121,7 @@ Fixpoint sep_pow (n: nat) (P: iProp Σ) : iProp Σ :=
 Lemma sep_pow_additive (a b : nat) (Q: iProp Σ)
     : sep_pow (a + b) Q ≡ (sep_pow a Q ∗ sep_pow b Q)%I.
 Proof.
-  induction b.
+  induction b as [|b IHb].
   - simpl. replace (a + 0) with a by lia.
     iIntros. iSplit. { iIntros "a".  iFrame. } iIntros "[a b]". iFrame.
   - simpl. replace (a + S b) with (S (a + b)) by lia. simpl.
@@ -162,32 +142,24 @@ Proof.  split.
   intros a b x. unfold "⋅", nat_op_instance. unfold family. apply sep_pow_additive.
 Qed.
 
-Definition m (γ: gname) (Q: iProp Σ) := maps γ (family Q).
+Definition m (γ: gname) (Q: iProp Σ) := sp_sto (sp_i := count_sp_inG) γ (family Q).
 
-Definition own_counter (γ: gname) (z: Z) := @p_own
-    nat _ _ _ _ _ Co _ _ _ _ _ _ _ _
-    count_storage_mixin Σ _
-    γ (Counters z 0).
+Definition own_counter (γ: gname) (z: Z) := sp_own (sp_i := count_sp_inG) γ (Counters z 0).
     
-Definition own_ref (γ: gname) := @p_own
-    nat _ _ _ _ _ Co _ _ _ _ _ _ _ _
-    count_storage_mixin Σ _
-    γ (Refs 1).
+Definition own_ref (γ: gname) := sp_own (sp_i := count_sp_inG) γ (Refs 1).
 
 Lemma count_init E (Q: iProp Σ)
   : ⊢ True ={E}=∗ ∃ (γ: gname) , m γ Q.
 Proof.
   iIntros "t".
-  iDestruct (@logic_init_ns nat _ _ _ _ _ Co _ _ _ _ _ _ _ _ _
-      count_storage_mixin Σ _ _
-      (Refs 0)
+  iDestruct (sp_alloc_ns (sp_i := count_sp_inG) (Refs 0) ε
       (family Q)
       E
       COUNT_NAMESPACE
       with "[t]") as "x".
-  { unfold pinv, co_inv. trivial. }
+  { unfold sp_inv, co_inv. split; trivial. unfold sp_inv. trivial. }
   { apply wf_prop_map_family. }
-  { unfold family. unfold interp, co_interp_instance. unfold sep_pow. iFrame. }
+  { unfold family. unfold sp_interp, co_interp_instance. unfold sep_pow. iFrame. }
   iMod "x". iModIntro.
   iDestruct "x" as (γ) "[%inn [a b]]".
   iExists γ.
@@ -198,21 +170,21 @@ Lemma co_deposit (R: iProp Σ) γ
   : m γ R ⊢ R ={{[γ]}}=∗ own_counter γ 0.
 Proof.
   iIntros "#m q".
-  iDestruct (logic_deposit (Refs 0) (Counters 0 0) 1 _ _ with "m [q]") as "x".
-  { unfold storage_protocol_deposit. intros q Y. split.
-    { unfold pinv, co_inv in *. destruct q.
+  iDestruct (sp_deposit (Refs 0) (Counters 0 0) 1 _ _ with "m [q]") as "x".
+  { rewrite eq_storage_protocol_deposit_ii. intros q Y. split.
+    { unfold sp_inv, co_inv in *. destruct q.
       { unfold "⋅", co_op, "⋅", co_op in *. lia. }
       { unfold "⋅", co_op, "⋅", co_op in *. lia. }
     }
     split.
     { unfold "✓", nat_valid_instance. trivial. }
-    { unfold interp, co_interp_instance, "⋅", co_op in *.
+    { unfold sp_interp, co_interp_instance, "⋅", co_op in *.
         destruct q.
         { unfold "⋅", co_op, "≡", nat_equiv_instance, nat_op_instance. lia. }
         unfold nat_op_instance. f_equiv. simpl. trivial.
     }
   }
-  { iSplitR. { iDestruct (p_own_unit with "m") as "u". unfold ε, co_unit. iFrame "u". }
+  { iSplitR. { iDestruct (sp_own_unit with "m") as "u". unfold ε, co_unit. iFrame "u". }
       { iModIntro. unfold family, sep_pow, sep_pow. iFrame "q". }
   }
   iMod "x". iModIntro. iFrame "x".
@@ -221,7 +193,7 @@ Qed.
 Lemma co_join z γ :
   (own_counter γ z) ∗ (own_ref γ) ⊣⊢ own_counter γ (z - 1).
 Proof.
-  setoid_rewrite <- p_own_op.
+  setoid_rewrite <- sp_own_op.
   unfold own_counter.
   trivial.
 Qed.
@@ -230,13 +202,13 @@ Lemma co_withdraw (R: iProp Σ) γ :
   m γ R ⊢ own_counter γ 0 ={{[γ]}}=∗ ▷ R.
 Proof.
   iIntros "#m q".
-  iDestruct (logic_withdraw (Counters 0 0) (Refs 0) 1 _ _ with "m [q]") as "x".
-  { unfold storage_protocol_withdraw. intros q Y. split.
-    { unfold pinv, co_inv in *. destruct q.
+  iDestruct (sp_withdraw (Counters 0 0) (Refs 0) 1 _ _ with "m [q]") as "x".
+  { rewrite eq_storage_protocol_withdraw_ii. intros q Y. split.
+    { unfold sp_inv, co_inv in *. destruct q.
       { unfold "⋅", co_op in *. lia. }
       { unfold "⋅", co_op in *. lia. }
     }
-    unfold interp, co_interp_instance, "⋅", co_op, nat_op_instance. destruct q.
+    unfold sp_interp, co_interp_instance, "⋅", co_op, nat_op_instance. destruct q.
       - f_equal.
       - f_equal.
   } 
@@ -258,14 +230,14 @@ Proof.
     unfold family, sep_pow. iIntros. iSplit. { iIntros. iFrame. } iIntros "[x y]". iFrame.
   }
   setoid_rewrite X at 2.
-  apply logic_guard.
+  apply sp_guard.
   2: { set_solver. }
-  unfold storage_protocol_guards. intro co. unfold "≼", pinv, co_inv.
+  rewrite eq_storage_protocol_guards_ii. intro co. unfold "≼", sp_inv, co_inv.
   intro Y. apply nat_ge_to_exists.
   unfold "⋅" in *.
   unfold co_op in *. destruct co.
   - lia.
-  - unfold interp, co_interp_instance. lia.
+  - unfold sp_interp, co_interp_instance. lia.
 Qed.
 
 End Counting.
diff --git a/src/examples/forever.v b/src/examples/forever.v
index f1e2a8c..efd928e 100644
--- a/src/examples/forever.v
+++ b/src/examples/forever.v
@@ -1,5 +1,4 @@
 From iris.base_logic.lib Require Import invariants.
-From lang Require Import lang simp adequacy primitive_laws.
 
 From iris.base_logic Require Export base_logic.
 From iris.program_logic Require Export weakestpre.
@@ -10,15 +9,12 @@ From iris.proofmode Require Import reduction.
 From iris.proofmode Require Import ltac_tactics.
 From iris.proofmode Require Import class_instances.
 From iris.program_logic Require Import ectx_lifting.
-From lang Require Import notation tactics class_instances.
-From lang Require Import heap_ra.
-From lang Require Import lang.
 From iris Require Import options.
 
 Require Import guarding.guard.
+Require Import guarding.tactics.
 Require Import examples.misc_tactics.
 Require Import guarding.storage_protocol.protocol.
-Require Import guarding.storage_protocol.inved.
 From iris.algebra Require Import auth.
 
 (** This file shows how to derive the rule
@@ -31,9 +27,6 @@ using a storage protocol. However, this rule is now part of the Leaf core logic,
 only useful academically for an understanding of how storage protocols work.
 *)
 
-Context {Σ: gFunctors}.
-Context `{!simpGS Σ}.
-
 Definition FOREVER_NAMESPACE := nroot .@ "forever".
 
 Inductive Trivial := Triv.
@@ -77,20 +70,20 @@ Global Instance exc_pcore A : PCore (Exc A) := λ a , None.
 Global Instance equ_exc : @Equivalence (Exc ()) (≡).
 Proof. split.
   - unfold Reflexive. intro x. destruct x; trivial.
-  - unfold Symmetric. intro x. destruct x, y; trivial.
-  - unfold Transitive. intro x. destruct x, y, z; trivial.
+  - unfold Symmetric. intros x y. destruct x, y; trivial.
+  - unfold Transitive. intros x y z. destruct x, y, z; trivial.
 Qed.
 
 Definition exc_ra_mixin {A} `{Equiv A} `{@Equivalence A (≡)} : RAMixin (Exc A).
 Proof. split.
- - intros. unfold Proper, "==>".  intros x0 y. destruct x0, x, y; trivial.
+ - intros x. unfold Proper, "==>".  intros x0 y. destruct x0, x, y; trivial.
     unfold "⋅", exc_op. intro. unfold "≡", exc_equiv. trivial.
  - unfold pcore, exc_pcore. intros. discriminate.
  - unfold Proper, equiv, "==>", valid, exc_equiv, exc_valid, impl. intros x y.
       destruct x; destruct y; trivial.
- - unfold Assoc. intros. unfold "⋅", exc_op. destruct x, y, z; trivial;
+ - unfold Assoc. intros x y z. unfold "⋅", exc_op. destruct x, y, z; trivial;
     unfold "≡", exc_equiv; trivial.
- - unfold Comm. intros. unfold "⋅", exc_op. destruct x, y; trivial;
+ - unfold Comm. intros x y. unfold "⋅", exc_op. destruct x, y; trivial;
     unfold "≡", exc_equiv; trivial.
  - unfold pcore, exc_pcore. intros. discriminate.
  - unfold pcore, exc_pcore. intros. discriminate.
@@ -104,14 +97,14 @@ Global Instance trivial_equiv : Equiv Trivial := λ a b , a = b.
 Global Instance trivial_pcore : PCore Trivial := λ a , None.
 Global Instance trivial_valid : Valid Trivial := λ a , True.
 Global Instance trivial_op : Op Trivial := λ a b , Triv.
-Global Instance trivial_pinv : PInv Trivial := λ a , True.
+Global Instance trivial_pinv : SPInv Trivial := λ a , True.
 
 Instance trivial_unit : Unit Trivial := Triv.
 
-Global Instance trivial_interp : Interp Trivial (Exc ()) := λ t , Yes ().
+Global Instance trivial_interp : SPInterp Trivial (Exc ()) := λ t , Yes ().
 
-Lemma trivial_valid_interp (p: Trivial) : ✓ (interp p : Exc ()).
-Proof. unfold "✓", exc_valid, interp, trivial_interp. trivial. Qed.
+Lemma trivial_valid_interp (p: Trivial) : ✓ (sp_interp p : Exc ()).
+Proof. unfold "✓", exc_valid, sp_interp, trivial_interp. trivial. Qed.
 
 Definition trivial_ra_mixin : RAMixin Trivial.
 Proof. split.
@@ -126,34 +119,25 @@ Proof. split.
   - trivial.
 Qed.
 
-Definition trivial_protocol_mixin : ProtocolMixin Trivial.
+Definition trivial_storage_mixin_ii : StorageMixinII Trivial (Exc ()).
 Proof. split.
   - apply trivial_ra_mixin.
-  - unfold LeftId. intro. destruct x; trivial.
-  - intro p. destruct p. intro. trivial.
-  - unfold Proper, "==>", impl. intros x y. destruct y. trivial.
-Qed.
-
-Definition trivial_storage_mixin : StorageMixin Trivial (Exc ()).
-Proof. split.
-  - apply trivial_protocol_mixin.
   - apply exc_ra_mixin.
   - unfold LeftId. intro x. destruct x; trivial.
-  - unfold Proper, "==>". intros x y. destruct x, y. trivial.
-  - intros. destruct p. trivial.
+  - unfold LeftId. intro x. destruct x; trivial.
+  - intro p. destruct p. intro. trivial.
+  - unfold Proper, "==>", impl. intros x y. destruct y. trivial.
+  - intros p. destruct p. trivial.
 Qed.
 
 Class forever_logicG Σ :=
     {
-      forever_logic_inG : inG Σ 
-        (authUR (inved_protocolUR (protocol_mixin (Trivial) (Exc ()) (trivial_storage_mixin))))
+      #[local] forever_sp_inG ::
+        sp_logicG (storage_mixin_from_ii trivial_storage_mixin_ii) Σ
     }.
-Local Existing Instance forever_logic_inG.
-
 
 Definition forever_logicΣ : gFunctors := #[
-  GFunctor
-        (authUR (inved_protocolUR (protocol_mixin (Trivial) (Exc ()) (trivial_storage_mixin))))
+  sp_logicΣ (storage_mixin_from_ii trivial_storage_mixin_ii)
 ].
 
 Global Instance subG_forever_logicΣ {Σ} : subG forever_logicΣ Σ → forever_logicG Σ.
@@ -162,7 +146,7 @@ Proof. solve_inG. Qed.
 Section Forever.
 
 Context {Σ: gFunctors}.
-Context `{@forever_logicG Σ}.
+Context `{f_in_Σ: @forever_logicG Σ}.
 Context `{!invGS Σ}.
 
 Definition family (Q: iProp Σ) (e: Exc ()) : iProp Σ :=
@@ -195,38 +179,29 @@ Qed.
 Lemma storage_protocol_guards_triv
   : storage_protocol_guards (ε: Trivial) (Yes ()).
 Proof.
-  unfold storage_protocol_guards. intro q. destruct q. unfold "⋅", trivial_op. unfold interp.
-  unfold trivial_interp. intro. unfold "≼". exists ε. trivial.
+  unfold storage_protocol_guards. intro q. destruct q. unfold "⋅", trivial_op.
+  intros t [spr speq]. exists (ε). setoid_rewrite <- speq. trivial.
 Qed.
 
 Lemma make_forever (Q: iProp Σ) (E: coPset)
   : ⊢ Q ={E}=∗ (True &&{↑ FOREVER_NAMESPACE : coPset}&&> ▷ Q).
-Proof using H invGS0 Σ.
+Proof using f_in_Σ.
   iIntros "q".
-  replace (Q) with (family Q (interp ε)) at 1 by trivial.
-  assert (@pinv Trivial trivial_pinv ε) as J.
-  { unfold pinv, ε, trivial_unit, trivial_pinv. trivial. }
-  iMod (logic_init_ns (ε : Trivial) (family Q) E (FOREVER_NAMESPACE) J with "q") as "r".
+  replace (Q) with (family Q (sp_interp ε)) at 1 by trivial.
+  assert (@sp_inv Trivial trivial_pinv ε) as J.
+  { unfold sp_inv, ε, trivial_unit, trivial_pinv. trivial. }
+  iMod (sp_alloc_ns (ε : Trivial) (Yes ()) (family Q) E (FOREVER_NAMESPACE) with "q") as "r". { split; trivial. }
   { apply wf_prop_map_family. }
   iDestruct "r" as (γ) "[%inns [#m p]]".
-  iDestruct (logic_guard (ε : Trivial) (Yes ()) γ (↑ FOREVER_NAMESPACE) (family Q) with "m")
+  iDestruct (sp_guard (ε : Trivial) (Yes ()) γ (↑ FOREVER_NAMESPACE) (family Q) with "m")
       as "g".
   { apply storage_protocol_guards_triv. }
   { trivial. }
   unfold family at 2.
-  iDestruct (p_own_unit with "m") as "u".
-  iDestruct (guards_refl (↑FOREVER_NAMESPACE) (True)%I) as "tt".
-  Set Printing Implicit.
-  iDestruct (guards_include_pers (□ p_own γ (@ε Trivial trivial_unit)) (True)%I (True)%I
-      (↑FOREVER_NAMESPACE) with "[p tt]") as "tu".
-      { iFrame "tt". iModIntro. iFrame "u". }
-  assert ((True ∗ □ p_own γ (ε: Trivial))%I ⊣⊢ ((p_own γ (ε: Trivial)) ∗ □ p_own γ (ε: Trivial))%I) as Z.
-  { iIntros. iSplit. { iIntros "[t #o]". iFrame "o". } { iIntros "[p #o]". iFrame "o". } }
-  rewrite Z.
-  iDestruct (guards_weaken_rhs_l with "tu") as "tk".
-  iModIntro.
-  iApply guards_transitive.
-  { iFrame "tk". iFrame "g". }
+  iDestruct (sp_own_unit with "m") as "u".
+  leaf_hyp "g" lhs to (True)%I as "g1".
+  - leaf_by_sep. iIntros. iFrame "#". iIntros. done.
+  - iFrame "g1". iModIntro. done.
 Qed.
 
 End Forever.
diff --git a/src/examples/fractional.v b/src/examples/fractional.v
index 2a2f461..d4aca3e 100644
--- a/src/examples/fractional.v
+++ b/src/examples/fractional.v
@@ -6,7 +6,6 @@ Require Import Coq.ZArith.Int.
 Undelimit Scope Int_scope.
 
 From iris.base_logic.lib Require Import invariants.
-From lang Require Import lang simp adequacy primitive_laws.
 
 From iris.base_logic Require Export base_logic.
 From iris.program_logic Require Export weakestpre.
@@ -17,21 +16,16 @@ From iris.proofmode Require Import reduction.
 From iris.proofmode Require Import ltac_tactics.
 From iris.proofmode Require Import class_instances.
 From iris.program_logic Require Import ectx_lifting.
-From lang Require Import notation tactics class_instances.
-From lang Require Import heap_ra.
-From lang Require Import lang.
 From iris Require Import options.
 
 Require Import guarding.guard.
 Require Import guarding.storage_protocol.protocol.
-Require Import guarding.storage_protocol.inved.
 From iris.algebra Require Import auth.
 
 Require Import examples.misc_tactics.
 
-
 Context {Σ: gFunctors}.
-Context `{!simpGS Σ}.
+Context `{!invGS Σ}.
 
 Definition FRAC_NAMESPACE := nroot .@ "fractional".
 
@@ -40,7 +34,7 @@ Definition frac := option Qp.
 Definition is_int (q: Qp) :=
     inject_Z (Qceiling (Qp_to_Qc q)) == Qp_to_Qc q.
 
-Global Instance frac_inv : PInv frac := λ t , match t with
+Global Instance frac_inv : SPInv frac := λ t , match t with
   | None => True
   | Some q => is_int q
 end.
@@ -85,29 +79,27 @@ Instance option_equiv {T} `{p: Equiv T} : Equiv (option T) := λ a b ,
 Definition option_ra_mixin {T} `{Equiv T, PCore T, Op T, Valid T} {equ: @Equivalence T (≡)} (m: RAMixin T)
     : RAMixin (option T).
 Proof.
-  destruct m. split.
-  - intro. unfold Proper, "==>". intros. destruct x, x0, y; trivial.
+  split.
+  - intro x. unfold Proper, "==>". intros x0 y Heq. destruct x, x0, y; trivial.
       + unfold "⋅", option_op. unfold "≡", option_equiv.
-          unfold "≡", option_equiv in H3.
-          apply ra_op_proper. trivial.
-      + unfold "≡", option_equiv in H3. contradiction.
-      + unfold "≡", option_equiv in H3. contradiction.
+          unfold "≡", option_equiv in Heq.
+          apply (ra_op_proper _ m). trivial.
+      + unfold "≡", option_equiv in Heq. contradiction.
+      + unfold "≡", option_equiv in Heq. contradiction.
       + unfold "≡", "⋅", option_equiv, option_op. trivial.
   - intros x y cx h j. unfold pcore, option_pcore in j. discriminate.
   - unfold Proper, "==>", impl. intros x y J. destruct x, y; trivial.
-      + unfold "✓", option_valid. apply ra_validN_proper.
+      + unfold "✓", option_valid. apply (ra_validN_proper _ m).
           unfold "≡", option_equiv in J. trivial.
       + intro. unfold "✓", option_valid. trivial.
       + unfold "≡", option_equiv in J. contradiction.
-  - unfold Assoc. intros x y z. destruct x, y, z; unfold "⋅", option_op, "≡", option_equiv;
-      trivial.
-  - unfold Comm. intros x y. destruct x, y; unfold "⋅", option_op, "≡", option_equiv;
-      trivial.
+  - destruct m. unfold Assoc. intros x y z. destruct x, y, z; unfold "⋅", option_op, "≡", option_equiv; trivial.
+  - destruct m. unfold Comm. intros x y. destruct x, y; unfold "⋅", option_op, "≡", option_equiv; trivial.
   - intros x cx X. unfold pcore, option_pcore in X. discriminate.
   - intros x cx X. unfold pcore, option_pcore in X. discriminate.
   - intros x y cx r X. unfold pcore, option_pcore in X. discriminate.
   - unfold "✓", option_valid, "⋅", option_op. intros x y X. destruct x, y; trivial.
-      apply (ra_valid_op_l _ _ X). 
+      apply (ra_valid_op_l _ m _ _ X). 
 Qed.
   
 Local Instance frac_valid_instance : Valid Qp := λ x, True.
@@ -148,49 +140,38 @@ Proof.
   (*- unfold Assoc. intros; unfold "⋅", nat_op_instance, "≡", nat_equiv_instance. lia.
   - unfold Comm. intros; unfold "⋅", nat_op_instance, "≡", nat_equiv_instance. lia.*)
 Qed.
-
-Definition frac_protocol_mixin : @ProtocolMixin (option Qp)
-      option_equiv option_pcore option_op option_valid _ _ _.
-Proof. split.
-  - exact (option_ra_mixin frac_ra_mixin).
-  - unfold LeftId. intros x. unfold ε, option_unit, "⋅", option_op, "≡", option_equiv.
-      destruct x; trivial.
-  - intros p X. unfold "✓", option_valid. destruct p; trivial. unfold "✓", frac_valid_instance.
-      trivial.
-  - unfold Proper, "==>", impl. intros x y X. unfold "≡", option_equiv in X.
-      destruct x, y; trivial.
-      + unfold "≡", frac_equiv_instance in X.  subst q. trivial.
-      + contradiction.
-      + contradiction.
-Qed.
   
-Local Instance frac_interp_instance : Interp (option Qp) nat := λ qopt , 
+Local Instance frac_interp_instance : SPInterp (option Qp) nat := λ qopt , 
   match qopt with
   | None => 0%nat
   | Some q => Z.to_nat (Qceiling (Qp_to_Qc q))
   end.
 
-Definition frac_storage_mixin : @StorageMixin (option Qp) nat
-    option_equiv option_pcore option_op option_valid _ _ _ _ _ _ _ _ _.
+Global Instance frac_storage_mixin_ii : @StorageMixinII (option Qp) nat
+    option_equiv option_pcore option_op option_valid _ _ _ _ _ _ _ _ _ _.
 Proof. split.
-  - exact frac_protocol_mixin.
-  - apply nat_ra_mixin.
+  - exact (option_ra_mixin frac_ra_mixin).
+  - exact nat_ra_mixin.
+  - unfold LeftId. intros x. unfold ε, option_unit, "⋅", option_op, "≡", option_equiv.
+      destruct x; trivial.
   - unfold LeftId. intros x. unfold ε, nat_unit_instance, "⋅", nat_op_instance. trivial.
-  - unfold Proper, "==>". intros. unfold "≡", option_equiv in H. destruct x, y; trivial; try contradiction. unfold "≡", frac_equiv_instance in H. subst q. trivial.
+  - intros p X eq. destruct p; trivial.
+      + unfold sp_inv, frac_inv. destruct X as [X|].
+        * inversion eq. trivial.
+        * inversion eq.
+      + destruct X. * inversion eq. * trivial.
+  - unfold Proper, "==>". intros x y Heq. unfold "≡", option_equiv in Heq. destruct x, y; trivial; try contradiction. unfold "≡", frac_equiv_instance in Heq. rewrite Heq. trivial.
   - intros. unfold "✓", nat_valid_instance. trivial.
 Qed.
 
 Class frac_logicG Σ :=
     {
-      frac_logic_inG : inG Σ 
-        (authUR (inved_protocolUR (protocol_mixin (option Qp) (nat) (frac_storage_mixin))))
+      #[local] frac_sp_inG ::
+        sp_logicG (storage_mixin_from_ii frac_storage_mixin_ii) Σ
     }.
-Local Existing Instance frac_logic_inG.
-
 
 Definition frac_logicΣ : gFunctors := #[
-  GFunctor
-        (authUR (inved_protocolUR (protocol_mixin (option Qp) (nat) (frac_storage_mixin))))
+  sp_logicΣ (storage_mixin_from_ii frac_storage_mixin_ii)
 ].
 
 Global Instance subG_frac_logicΣ {Σ} : subG frac_logicΣ Σ → frac_logicG Σ.
@@ -211,7 +192,7 @@ Fixpoint sep_pow (n: nat) (P: iProp Σ) : iProp Σ :=
 Lemma sep_pow_additive (a b : nat) (Q: iProp Σ)
     : sep_pow (a + b) Q ≡ (sep_pow a Q ∗ sep_pow b Q)%I.
 Proof.
-  induction b.
+  induction b as [|b IHb].
   - simpl. replace (a + 0) with a by lia.
     iIntros. iSplit. { iIntros "a".  iFrame. } iIntros "[a b]". iFrame.
   - simpl. replace (a + S b) with (S (a + b)) by lia. simpl.
@@ -232,35 +213,29 @@ Proof.  split.
   intros a b x. unfold "⋅", nat_op_instance. unfold family. apply sep_pow_additive.
 Qed.
 
-Definition m (γ: gname) (Q: iProp Σ) := @maps
-      nat _ _ _ _ _ frac _ _ _ _ _ _ _ _ frac_storage_mixin Σ _ _
-  γ (family Q).
+Definition m (γ: gname) (Q: iProp Σ) := sp_sto (sp_i := frac_sp_inG) γ (family Q).
 
-Definition own_frac (γ: gname) (qp: Qp) := @p_own
-    nat _ _ _ _ _ (option Qp) _ _ _ _ _ _ _ _
-    frac_storage_mixin Σ _
-    γ (Some qp).
+Definition own_frac (γ: gname) (qp: Qp) := sp_own (sp_i := frac_sp_inG) γ (Some qp).
 
 Lemma frac_init E (Q: iProp Σ)
   : ⊢ True ={E}=∗ ∃ (γ: gname) , m γ Q.
 Proof.
   iIntros "t".
-  iDestruct (@logic_init_ns nat _ _ _ _ _ (option Qp) _ _ _ _ _ _ _ _ _
-      frac_storage_mixin Σ _ _
+  iDestruct (sp_alloc_ns (sp_i := frac_sp_inG)
       (None : option Qp)
+      ε
       (family Q)
       E
       FRAC_NAMESPACE
       with "[t]") as "x".
-  { unfold pinv, frac_inv. trivial. }
+  { unfold sp_inv, frac_inv. split; trivial. unfold sp_inv. trivial. }
   { apply wf_prop_map_family. }
-  { unfold family. unfold interp, frac_interp_instance. unfold sep_pow. iFrame. }
+  { unfold family. unfold sp_interp, frac_interp_instance. unfold sep_pow. iFrame. }
   iMod "x". iModIntro.
   iDestruct "x" as (γ) "[%inn [a b]]".
   iExists γ.
   iFrame "a".
 Qed.
- 
 
 Lemma q_le_add_1 (a b: Q) (is_le: Qle a b) : Qle (a + 1) (b + 1).
   Proof. rewrite Qplus_le_l. trivial. Qed.
@@ -271,7 +246,7 @@ Lemma injz_p1 (z: Z) : inject_Z z + 1 == inject_Z (z + 1). Proof.
   replace (inject_Z 1) with (1%Q). - apply Qeq_refl. - simpl. trivial. Qed.
   
 Lemma Qceiling_plus_1 q : (Qceiling (q + 1))%Z = (Qceiling q + 1)%Z. 
-Proof using H invGS0 Σ.
+Proof.
   have h1 := Qle_ceiling q. have h2 := Qle_ceiling (q + 1).
   have h3 := Qceiling_lt q. have h4 := Qceiling_lt (q + 1).
   have h1' := q_le_add_1 _ _ h1. have h3' := q_lt_add_1 _ _ h3.
@@ -285,7 +260,7 @@ Qed.
 
 Lemma is_int_plus_1 (q: Qp)
   (q_is_int : is_int q) : is_int (1%Qp + q).
-Proof using H invGS0 Σ.
+Proof.
   unfold is_int in *.
   assert ((Qceiling (Qp_to_Qc (1 + q))) = Z.add 1 (Qceiling (Qp_to_Qc q))) as Y.
   2: {
@@ -315,7 +290,7 @@ Qed.
  
 Lemma is_int_minus_1 (q: Qp)
   (q_p1_is_int : is_int (1 + q)) : is_int q.
-Proof using H invGS0 Σ.
+Proof.
   unfold is_int in *.
   assert ((Qceiling (Qp_to_Qc (1 + q))) = Z.add 1 (Qceiling (Qp_to_Qc q))) as Y.
   2: {
@@ -384,7 +359,7 @@ Proof. have h := ceil_ge_1 q. lia. Qed.
 
 Lemma to_nat_add_1 (q: Qp) :
   Z.to_nat (Qceiling (Qp_to_Qc q)) + 1 = Z.to_nat (Qceiling (Qp_to_Qc (1 + q))).
-Proof using H invGS0 Σ.
+Proof.
   rewrite <- Z_to_nat_plus_1 by apply Qceiling_qp_ge_0.
   f_equal.
   rewrite <- Qceiling_plus_1.
@@ -406,21 +381,21 @@ Lemma frac_deposit (R: iProp Σ) γ
   : m γ R ⊢ R ={{[γ]}}=∗ own_frac γ 1.
 Proof.
   iIntros "#m q".
-  iDestruct (logic_deposit None (Some (1%Qp)) 1 _ _ with "m [q]") as "x".
-  { unfold storage_protocol_deposit. intros q Y. split.
-    { unfold pinv, frac_inv in *. destruct q.
+  iDestruct (sp_deposit None (Some (1%Qp)) 1 _ _ with "m [q]") as "x".
+  { rewrite eq_storage_protocol_deposit_ii. intros q Y. split.
+    { unfold sp_inv, frac_inv in *. destruct q.
       { unfold "⋅", option_op, "⋅", frac_op_instance in *. apply is_int_plus_1. trivial. }
       { unfold "⋅", option_op, "⋅", frac_op_instance in *. apply is_int_1. }
     }
     split.
     { unfold "✓", nat_valid_instance. trivial. }
-    { unfold interp, frac_interp_instance, "⋅", option_op, nat_op_instance in *.
+    { unfold sp_interp, frac_interp_instance, "⋅", option_op, nat_op_instance in *.
         destruct q.
         { unfold "⋅", frac_op_instance, "≡", nat_equiv_instance.
             apply to_nat_add_1. }
         simpl. trivial. } 
   }
-  { iSplitR. { iDestruct (p_own_unit with "m") as "u". unfold ε, option_unit. iFrame "u". }
+  { iSplitR. { iDestruct (sp_own_unit with "m") as "u". unfold ε, option_unit. iFrame "u". }
       { iModIntro. unfold family, sep_pow, sep_pow. iFrame "q". }
   }
   iMod "x". iModIntro. iFrame "x".
@@ -429,7 +404,7 @@ Qed.
 Lemma frac_join q1 q2 γ :
   (own_frac γ q1) ∗ (own_frac γ q2) ⊣⊢ own_frac γ (q1 + q2).
 Proof.
-  setoid_rewrite <- p_own_op.
+  setoid_rewrite <- sp_own_op.
   unfold own_frac.
   trivial.
 Qed.
@@ -438,13 +413,13 @@ Lemma frac_withdraw (R: iProp Σ) γ :
   m γ R ⊢ own_frac γ 1 ={{[γ]}}=∗ ▷ R.
 Proof.
   iIntros "#m q".
-  iDestruct (logic_withdraw (Some (1%Qp)) None 1 _ _ with "m [q]") as "x".
-  { unfold storage_protocol_withdraw. intros q Y. split.
-    { unfold pinv, frac_inv in *. destruct q.
+  iDestruct (sp_withdraw (Some (1%Qp)) None 1 _ _ with "m [q]") as "x".
+  { rewrite eq_storage_protocol_withdraw_ii. intros q Y. split.
+    { unfold sp_inv, frac_inv in *. destruct q.
       { unfold "⋅", option_op, "⋅", frac_op_instance in *. apply is_int_minus_1. trivial. }
       { unfold "⋅", option_op, "⋅", frac_op_instance in *. trivial. }
     }
-    unfold interp, frac_interp_instance, "⋅", option_op, nat_op_instance. destruct q.
+    unfold sp_interp, frac_interp_instance, "⋅", option_op, nat_op_instance. destruct q.
     - symmetry. apply to_nat_add_1.
     - simpl. trivial. }
   { iFrame "q". }
@@ -462,11 +437,11 @@ Proof.
     unfold family, sep_pow. iIntros. iSplit. { iIntros. iFrame. } iIntros "[x y]". iFrame.
   }
   setoid_rewrite X at 2.
-  apply logic_guard.
+  apply sp_guard.
   2: { set_solver. }
-  unfold storage_protocol_guards. intro q0. unfold "≼", pinv, frac_inv.
+  rewrite eq_storage_protocol_guards_ii. intro q0. unfold "≼", sp_inv, frac_inv.
   intro.
-  apply nat_ge_to_exists. unfold interp, frac_interp_instance, "⋅", option_op.
+  apply nat_ge_to_exists. unfold sp_interp, frac_interp_instance, "⋅", option_op.
   destruct q0.
   - apply nat_ceil_ge_1.
   - apply nat_ceil_ge_1.
diff --git a/src/guarding/storage_protocol/inved.v b/src/guarding/internal/inved.v
similarity index 87%
rename from src/guarding/storage_protocol/inved.v
rename to src/guarding/internal/inved.v
index 948863d..fd827ae 100644
--- a/src/guarding/storage_protocol/inved.v
+++ b/src/guarding/internal/inved.v
@@ -3,13 +3,8 @@ From iris.algebra Require Export cmra updates proofmode_classes.
 From iris.base_logic.lib Require Export own iprop.
 From iris.proofmode Require Import base ltac_tactics tactics coq_tactics reduction.
 
-(*
-Context {Σ: gFunctors}.
-Context `{!invGS Σ}.
-*)
-
-Class PInv (A : Type) := pinv : A → Prop.
-Global Hint Mode PInv ! : typeclass_instances.
+Class InternalPInv (A : Type) := pinv : A → Prop.
+Global Hint Mode InternalPInv ! : typeclass_instances.
 Global Instance: Params (@pinv) 2 := {}.
 
 Inductive InvedProtocol (P: Type) :=
@@ -40,13 +35,13 @@ Global Instance inved_protocol_pcore P `{PCore P} `{Unit P} : PCore (InvedProtoc
       | Nah => Some Nah
     end.
 
-Global Instance inved_protocol_valid P `{PInv P} `{Op P} : Valid (InvedProtocol P) | 0 :=
+Global Instance inved_protocol_valid P `{InternalPInv P} `{Op P} : Valid (InvedProtocol P) | 0 :=
    λ x , match x with
     | Inved a => ∃ b , pinv (a ⋅ b)
     | Nah => True
    end.
    
-Global Instance inved_protocol_op P `{PInv P} `{Op P} : Op (InvedProtocol P) | 0 :=
+Global Instance inved_protocol_op P `{InternalPInv P} `{Op P} : Op (InvedProtocol P) | 0 :=
    λ x y , 
     match x with
       | Inved a =>
@@ -66,7 +61,7 @@ Qed.
 *)
 
 Lemma inved_incl_to_incl {P} 
-    `{Equiv P, Op P, PInv P}
+    `{Equiv P, Op P, InternalPInv P}
     (a b : P) (mle : Inved a ≼ Inved b) : a ≼ b \/ b ≡ a.
 Proof.
   unfold "≼".
@@ -79,7 +74,7 @@ Proof.
 Qed.
 
 Lemma incl_to_inved_incl {P} 
-    `{Equiv P, Op P, PInv P}
+    `{Equiv P, Op P, InternalPInv P}
     (a b : P) (mle : a ≼ b) : Inved a ≼ Inved b.
 Proof.
   unfold "≼".
@@ -104,28 +99,24 @@ Proof.
       + intros a1 a2. setoid_rewrite a1. trivial.
 Qed.
 
-Record ProtocolMixin P
-    `{Equiv P, PCore P, Op P, Valid P, PInv P, Unit P}
+Record InternalProtocolMixin P
+    `{Equiv P, PCore P, Op P, Valid P, InternalPInv P, Unit P}
     {equ: @Equivalence P (≡)}
 := {
     protocol_ra_mixin: RAMixin P;
-    
     (*protocol_unit_valid : ✓ (ε : P);
     protocol_pcore_unit : pcore (ε : P) ≡ Some (ε : P);*)
-    
     protocol_unit_left_id : LeftId equiv (ε : P) op;
-    
-    inv_implies_valid: ∀ (p: P) , pinv p -> ✓ p;
-    inv_proper: Proper ((≡) ==> impl) (@pinv P _);
+    internal_inv_proper: Proper ((≡) ==> impl) (@pinv P _);
 }.
 
 Definition inved_protocol_ra_mixin {P}
-    `{Equiv P, PCore P, Op P, PInv P, Valid P, Unit P}
+    `{Equiv P, PCore P, Op P, InternalPInv P, Valid P, Unit P}
     {equ: @Equivalence P (≡)}
-    (protocol_mixin: ProtocolMixin P) : RAMixin (InvedProtocol P).
+    (internal_protocol_mixin: InternalProtocolMixin P) : RAMixin (InvedProtocol P).
 Proof.
-  destruct protocol_mixin as [protocol_ra_mixin0
-    protocol_unit_left_id0 inv_implies_valid0 inv_proper0].
+  destruct internal_protocol_mixin as [protocol_ra_mixin0
+    protocol_unit_left_id0 internal_inv_proper0].
   have protocol_ra_mixin1 := protocol_ra_mixin0.
   destruct protocol_ra_mixin0 as [ra_op_proper ra_core_proper ra_validN_proper ra_assoc ra_comm ra_pcore_l ra_pcore_idemp ra_pcore_mono ra_valid_op_l].
   split.
@@ -181,7 +172,7 @@ Proof.
     + inversion ipe.
     + intro h. destruct h as [b ipb]. exists b.
       unfold inved_protocol_equiv in ipe.
-      eapply inv_proper0. 2: { apply ipb. }
+      eapply internal_inv_proper0. 2: { apply ipb. }
       assert (p ⋅ b ≡ b ⋅ p) as X. { eapply ra_comm. }
       assert (p0 ⋅ b ≡ b ⋅ p0) as Y. { eapply ra_comm. }
       setoid_rewrite X. setoid_rewrite Y.
@@ -292,7 +283,7 @@ Proof.
       destruct eb as [b eb].
       exists (p0 ⋅ b).
 
-      eapply inv_proper0. 2: { apply eb. }
+      eapply internal_inv_proper0. 2: { apply eb. }
 
       symmetry. apply ra_assoc.
 Qed.
@@ -304,28 +295,28 @@ Canonical Structure inved_protocolO
     := discreteO (InvedProtocol P).
     
 Canonical Structure inved_protocolR {P}
-    `{Equiv P, PCore P, Op P, PInv P, Valid P, Unit P}
+    `{Equiv P, PCore P, Op P, InternalPInv P, Valid P, Unit P}
     {equ: Equivalence (≡@{P})}
-    (protocol_mixin: ProtocolMixin P)
+    (internal_protocol_mixin: InternalProtocolMixin P)
     :=
-   discreteR (InvedProtocol P) (inved_protocol_ra_mixin protocol_mixin). 
+   discreteR (InvedProtocol P) (inved_protocol_ra_mixin internal_protocol_mixin). 
 
 Global Instance inved_protocol_unit P : Unit (InvedProtocol P) := Nah.
 
 
 Definition inved_protocol_ucmra_mixin {P}
-    `{Equiv P, PCore P, Op P, PInv P, Valid P, Unit P}
+    `{Equiv P, PCore P, Op P, InternalPInv P, Valid P, Unit P}
     {equ: Equivalence (≡@{P})}
-    (protocol_mixin: ProtocolMixin P) :
+    (internal_protocol_mixin: InternalProtocolMixin P) :
       @UcmraMixin (InvedProtocol P)
-       (cmra_dist (inved_protocolR protocol_mixin))
+       (cmra_dist (inved_protocolR internal_protocol_mixin))
        (inved_protocol_equiv P)
        (inved_protocol_pcore P)
        (inved_protocol_op P)
        (inved_protocol_valid P)
        (inved_protocol_unit P).
 Proof.
-  destruct protocol_mixin.
+  destruct internal_protocol_mixin.
   split.
   - unfold ε, "✓", cmra_valid, inved_protocol_unit, inved_protocol_valid. trivial.
   - unfold LeftId, ε. intros. unfold inved_protocol_unit.
@@ -334,35 +325,19 @@ Proof.
 Qed.
 
 Canonical Structure inved_protocolUR {P}
-    `{Equiv P, PCore P, Op P, PInv P, Valid P, Unit P}
+    `{Equiv P, PCore P, Op P, InternalPInv P, Valid P, Unit P}
     {equ: Equivalence (≡@{P})}
-    (protocol_mixin: ProtocolMixin P) : ucmra
+    (internal_protocol_mixin: InternalProtocolMixin P) : ucmra
     :=
     @Ucmra'
       (InvedProtocol P)
        (inved_protocol_equiv P)
-       (cmra_dist (inved_protocolR protocol_mixin))
+       (cmra_dist (inved_protocolR internal_protocol_mixin))
        (inved_protocol_pcore P)
        (inved_protocol_op P)
        (inved_protocol_valid P)
-       (cmra_validN (inved_protocolR protocol_mixin))
+       (cmra_validN (inved_protocolR internal_protocol_mixin))
        (inved_protocol_unit P)
-       (cmra_ofe_mixin (inved_protocolR protocol_mixin))
-       (cmra_mixin (inved_protocolR protocol_mixin))
-      (inved_protocol_ucmra_mixin protocol_mixin).
-
-(*
-Section Inved.
-
-
-  Context `{Equiv P, PCore P, Op P, PInv P, Valid P, Unit P}.
-  Context {equ: Equivalence (≡@{P})}.
-  Context {protocol_mixin: ProtocolMixin P}.
-
-  Context {Σ: gFunctors}.
-  Context `{!inG Σ (authUR (inved_protocolUR protocol_mixin))}.
-  
-
-End Inved.
-
-*)
+       (cmra_ofe_mixin (inved_protocolR internal_protocol_mixin))
+       (cmra_mixin (inved_protocolR internal_protocol_mixin))
+      (inved_protocol_ucmra_mixin internal_protocol_mixin).
diff --git a/src/guarding/lib/rwlock.v b/src/guarding/lib/rwlock.v
index e125251..b28f502 100644
--- a/src/guarding/lib/rwlock.v
+++ b/src/guarding/lib/rwlock.v
@@ -2,7 +2,6 @@ From iris.prelude Require Import options.
 Require Import guarding.guard.
 Require Import guarding.storage_protocol.base_storage_opt.
 Require Import guarding.storage_protocol.protocol.
-Require Import guarding.storage_protocol.inved.
 Require Import stdpp.base.
 From iris.algebra Require Import cmra updates proofmode_classes auth.
 From iris.base_logic.lib Require Export own iprop invariants.
@@ -123,7 +122,7 @@ Definition free_count {S} `{!EqDecision S} (m: AgN S) : nat :=
   | Conflict => 0
   end.
   
-Instance rwlock_pinv {S} `{!EqDecision S} : PInv (RwLock S) :=
+Instance rwlock_sp_inv {S} `{!EqDecision S} : SPInv (RwLock S) :=
   λ rw ,
   match rw with
   | Rwl _ Fail _ _ _ => False
@@ -141,7 +140,7 @@ Instance rwlock_pinv {S} `{!EqDecision S} : PInv (RwLock S) :=
 Instance rwlock_unit (S: Type) `{!EqDecision S} : Unit (RwLock S) :=
   Rwl Unknown Unknown Unknown 0 Empty.
 
-Global Instance rwlock_interp (S: Type) `{!EqDecision S} : Interp (RwLock S) (BaseOpt S) :=
+Global Instance rwlock_interp (S: Type) `{!EqDecision S} : SPInterp (RwLock S) (BaseOpt S) :=
   λ rw , match rw with
     | Rwl (Yes (_,_,x)) _ Unknown _ _ => Full x
     | _ => base_storage_opt.Empty
@@ -166,18 +165,17 @@ Proof.
 Qed.
 
 Lemma rw_init_valid {S} `{!EqDecision S} (x: S)
-  : pinv (Central false 0 x).
+  : sp_inv (Central false 0 x).
 Proof.
-  unfold pinv, rwlock_pinv, Central, free_count. split; trivial.
+  unfold sp_inv, rwlock_sp_inv, Central, free_count. split; trivial.
   - intuition; discriminate.
 Qed.
 
-Arguments storage_protocol_update B%type_scope {H} {P}%type_scope {H6 H7 H10} _ _.
-
 Lemma rw_mov_exc_begin {S} `{!EqDecision S} rc x
-  : storage_protocol_update (BaseOpt S) (Central false rc x) (Central true rc x ⋅ ExcPending).
+  : storage_protocol_update_ii (B := BaseOpt S) (Central false rc x) (Central true rc x ⋅ ExcPending).
 Proof.
-  unfold storage_protocol_update. unfold pinv, rwlock_pinv, interp, rwlock_interp in *. intros p H.
+  unfold storage_protocol_update_ii.
+  unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp in *. intros p H.
   split.
     + unfold Central, ExcPending in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op in *. destruct e, e0, e1, a; try contradiction; intuition; try discriminate.
@@ -186,100 +184,101 @@ Proof.
 Qed.
 
 Lemma rw_mov_exc_acquire {S} `{!EqDecision S} (exc: bool) (x: S)
-  : storage_protocol_withdraw
+  : storage_protocol_withdraw_ii
     (Central exc 0 x ⋅ ExcPending)
     (Central exc 0 x ⋅ ExcGuard)
     (base_storage_opt.Full x).
 Proof.
-  unfold storage_protocol_withdraw. intro p. intro H. split.
-  - unfold pinv, rwlock_pinv, "⋅", rw_op, Central, ExcGuard, ExcPending in *. destruct p.
+  unfold storage_protocol_withdraw_ii.
+  intro p. intro H. split.
+  - unfold sp_inv, rwlock_sp_inv, "⋅", rw_op, Central, ExcGuard, ExcPending in *. destruct p.
       unfold "⋅", exc_op, free_op in *.
-      + destruct e, e0, e1, a; unfold pinv, rwlock_pinv in *; intuition; try destruct exc; try destruct u; intuition; unfold free_count in *; try lia; intuition; try discriminate.
-  - unfold pinv, rwlock_pinv, interp, rwlock_interp in *. unfold "⋅", Central, ExcPending, ExcGuard, rw_op in *.
+      + destruct e, e0, e1, a; unfold sp_inv, rwlock_sp_inv in *; intuition; try destruct exc; try destruct u; intuition; unfold free_count in *; try lia; intuition; try discriminate.
+  - unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp in *. unfold "⋅", Central, ExcPending, ExcGuard, rw_op in *.
       destruct p. unfold "⋅", free_op, exc_op in *. destruct e, e1, e0; trivial;
         try (rewrite unit_dot);
         try (rewrite unit_dot_left);
         try (apply reflex);
-        unfold pinv, rwlock_pinv in H; destruct a; try (destruct u); try (destruct exc); unfold ε, rwlock_unit in *; intuition; try (inversion H).
+        unfold sp_inv, rwlock_sp_inv in H; destruct a; try (destruct u); try (destruct exc); unfold ε, rwlock_unit in *; intuition; try (inversion H).
 Qed.
 
 Lemma rw_mov_exc_release {S} `{!EqDecision S} (exc: bool) (rc: Z) (x y: S)
-  : storage_protocol_deposit
+  : storage_protocol_deposit_ii
     (Central exc rc y ⋅ ExcGuard)
     (Central false rc x)
     (Full x).
 Proof.
-  unfold storage_protocol_deposit. intro p. intro H. split.
-  - unfold pinv, rwlock_pinv, interp, rwlock_interp, "⋅", rw_op, Central, ExcGuard, ExcPending in *. destruct p.
+  unfold storage_protocol_deposit_ii. intro p. intro H. split.
+  - unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp, "⋅", rw_op, Central, ExcGuard, ExcPending in *. destruct p.
       unfold "⋅", exc_op, free_op in *. 
-      destruct e, e0, e1, a; unfold pinv, rwlock_pinv; intuition; try destruct exc; try destruct u; try discriminate; intuition.
-  - unfold pinv, rwlock_pinv, interp, rwlock_interp in *. unfold "⋅", Central, ExcPending, ExcGuard, rw_op in *.
+      destruct e, e0, e1, a; unfold sp_inv, rwlock_sp_inv; intuition; try destruct exc; try destruct u; try discriminate; intuition.
+  - unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp in *. unfold "⋅", Central, ExcPending, ExcGuard, rw_op in *.
       destruct p. unfold "⋅", free_op, exc_op in *. destruct e, e1, e0; trivial;
         try (rewrite unit_dot);
         try (rewrite unit_dot_left);
         try (apply reflex);
-        unfold pinv, rwlock_pinv in H; destruct a; try (destruct u); try (destruct exc); unfold ε, rwlock_unit in *; intuition; try discriminate.
+        unfold sp_inv, rwlock_sp_inv in H; destruct a; try (destruct u); try (destruct exc); unfold ε, rwlock_unit in *; intuition; try discriminate.
 Qed.
 
 Lemma rw_mov_shared_begin {S} `{!EqDecision S} (exc: bool) (rc: Z) (x: S)
-  : storage_protocol_update (BaseOpt S)
+  : storage_protocol_update_ii (B := BaseOpt S)
     (Central exc rc x)
     (Central exc (rc + 1) x ⋅ ShPending).
 Proof.
-  unfold storage_protocol_update. intros p H. unfold pinv, rwlock_pinv, interp, rwlock_interp in *.
+  unfold storage_protocol_update. intros p H. unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp in *.
   split.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShPending in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShPending in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op, free_count in *. destruct e, e0, e1, a; try contradiction; try destruct exc; intuition; try lia.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShPending in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShPending in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op in *. destruct e, e0, e1, a; try contradiction; intuition; try discriminate.
 Qed.
 
 Lemma rw_mov_shared_acquire {S} `{!EqDecision S} (rc: Z) (x: S)
-  : storage_protocol_update (BaseOpt S)
+  : storage_protocol_update_ii (B := BaseOpt S)
     (Central false rc x ⋅ ShPending)
     (Central false rc x ⋅ ShGuard x).
 Proof.
-  unfold storage_protocol_update. intros p H. unfold pinv, rwlock_pinv, interp, rwlock_interp in *.
+  unfold storage_protocol_update_ii. intros p H. unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp in *.
   split.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShPending, ShGuard in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShPending, ShGuard in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op, free_count in *. destruct e, e0, e1, a; try contradiction; intuition; try lia; try discriminate.
         case_decide; intuition; try lia; try discriminate.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShPending, ShGuard in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShPending, ShGuard in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op in *. destruct e, e0, e1, a; try contradiction; intuition; try discriminate.
 Qed.
 
 Lemma rw_mov_shared_release {S} `{!EqDecision S} (exc: bool) (rc: Z) (x y: S)
-  : storage_protocol_update (BaseOpt S)
+  : storage_protocol_update_ii (B := BaseOpt S)
     (Central exc rc x ⋅ ShGuard y)
     (Central exc (rc - 1) x).
 Proof.
-  unfold storage_protocol_update. intros p H. unfold pinv, rwlock_pinv, interp, rwlock_interp in *.
+  unfold storage_protocol_update. intros p H. unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp in *.
   split.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShGuard in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShGuard in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op, free_count in *. destruct e, e0, e1, a, exc; try contradiction; try case_decide; intuition; try lia; try discriminate; try subst x; trivial.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShGuard in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShGuard in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op in *. destruct e, e0, e1, a; try contradiction; intuition; try discriminate.
 Qed.
 
 Lemma rw_mov_shared_retry {S} `{!EqDecision S} (exc: bool) (rc: Z) (x: S)
-  : storage_protocol_update (BaseOpt S)
+  : storage_protocol_update_ii (B := BaseOpt S)
     (Central exc rc x ⋅ ShPending)
     (Central exc (rc - 1) x).
 Proof.
-  unfold storage_protocol_update. intros p H. unfold pinv, rwlock_pinv, interp, rwlock_interp in *.
+  unfold storage_protocol_update_ii. intros p H. unfold sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp in *.
   split.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShPending in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShPending in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op, free_count in *. destruct e, e0, e1, a, exc; try contradiction; try case_decide; intuition; try lia.
-    + unfold pinv, rwlock_pinv in *. unfold Central, ShPending in *. destruct p.
+    + unfold sp_inv, rwlock_sp_inv in *. unfold Central, ShPending in *. destruct p.
       unfold "⋅", rw_op in *. unfold "⋅", exc_op, free_op in *. destruct e, e0, e1, a; try contradiction; intuition; try discriminate.
 Qed.
 
 Lemma rw_mov_shared_borrow {S} `{!EqDecision S} (x: S)
-  : storage_protocol_guards (ShGuard x) (Full x).
+  : storage_protocol_guards_ii (ShGuard x) (Full x).
 Proof.
-  unfold storage_protocol_guards. intros p H. unfold "≼". exists ε. rewrite base_opt_unit_right_id.
-  unfold ShGuard, "⋅", rw_op, pinv, rwlock_pinv, interp, rwlock_interp  in *. destruct p.
-  unfold "⋅", exc_op, free_op in *. unfold pinv, rwlock_pinv in H. destruct e, e0, e1, a; try contradiction;
+  unfold storage_protocol_guards_ii. intros p H. unfold "≼". exists ε. rewrite base_opt_unit_right_id.
+  unfold ShGuard, "⋅", rw_op, sp_inv, rwlock_sp_inv, sp_interp, rwlock_interp  in *. destruct p.
+  unfold "⋅", exc_op, free_op in *. unfold sp_inv, rwlock_sp_inv in H. destruct e, e0, e1, a; try contradiction;
       try (case_decide); try contradiction; try (destruct p); try (destruct p);
       try intuition; try (destruct u); try contradiction; unfold free_count in *; try lia;
       intuition; try discriminate; destruct b; intuition; intuition;
@@ -302,8 +301,8 @@ Global Instance rwlock_equiv {S} `{EqDecision S} : Equiv (RwLock S) := λ a b ,
 Global Instance rwlock_pcore {S} `{EqDecision S} : PCore (RwLock S) := λ a , None.
 Global Instance rwlock_valid {S} `{EqDecision S} : Valid (RwLock S) := λ a , True.
 
-Lemma rwlock_valid_interp {S} `{EqDecision S} (p: RwLock S) : ✓ interp p.
-Proof. destruct p. unfold "✓", base_opt_valid. unfold interp, rwlock_interp.
+Lemma rwlock_valid_interp {S} `{EqDecision S} (p: RwLock S) : ✓ sp_interp p.
+Proof. destruct p. unfold "✓", base_opt_valid. unfold sp_interp, rwlock_interp.
     destruct e; trivial. destruct p; trivial. destruct e1; trivial;
     destruct p; trivial.
 Qed.
@@ -321,32 +320,26 @@ Proof. split.
   - trivial.
 Qed.
 
-Definition rwlock_protocol_mixin S {eqdec: EqDecision S} : ProtocolMixin (RwLock S).
+Global Instance rwlock_storage_mixin_ii S {eqdec: EqDecision S} :
+    StorageMixinII (RwLock S) (BaseOpt S).
 Proof. split.
   - apply rwlock_ra_mixin.
-  - unfold LeftId. unfold "⋅". apply rw_unit_dot_left.
-  - intros. unfold "✓", rwlock_valid. trivial.
-  - typeclasses eauto.
-Qed.
-
-Definition rwlock_storage_mixin S {eqdec: EqDecision S} : StorageMixin (RwLock S) (BaseOpt S).
-Proof. split.
-  - apply rwlock_protocol_mixin.
   - apply base_opt_ra_mixin.
+  - unfold LeftId. unfold "⋅". apply rw_unit_dot_left.
   - unfold LeftId. apply base_opt_unit_left_id.
   - typeclasses eauto.
+  - typeclasses eauto.
   - intros. apply rwlock_valid_interp.
 Qed.
 
 Class rwlock_logicG {S: Type} {eqdec: EqDecision S} Σ :=
     {
-      #[global] rwlock_logic_inG :: inG Σ 
-        (authUR (inved_protocolUR (protocol_mixin (RwLock S) (BaseOpt S) (rwlock_storage_mixin S))))
+      #[local] rwlock_sp_inG ::
+        sp_logicG (storage_mixin_from_ii (rwlock_storage_mixin_ii S)) Σ
     }.
 
 Definition rwlock_logicΣ {S: Type} {eqdec: EqDecision S} : gFunctors := #[
-  GFunctor
-        (authUR (inved_protocolUR (protocol_mixin (RwLock S) (BaseOpt S) (rwlock_storage_mixin S))))
+  sp_logicΣ (storage_mixin_from_ii (rwlock_storage_mixin_ii S))
 ].
 
 Global Instance subG_rwlock_logicΣ {S: Type} {eqdec: EqDecision S} {Σ} :
@@ -363,16 +356,15 @@ Context {Σ: gFunctors}.
 Context `{@rwlock_logicG S _ Σ}.
 Context `{!invGS Σ}.
 
-Definition fields γ (e: bool) (r: Z) (x: S) : iProp Σ := p_own γ (Central e r x).
-Definition exc_pending γ : iProp Σ := p_own γ ExcPending.
-Definition exc_guard γ : iProp Σ := p_own γ ExcGuard.
-Definition sh_pending γ : iProp Σ := p_own γ ShPending.
-Definition sh_guard γ m : iProp Σ := p_own γ (ShGuard m).
+Definition fields γ (e: bool) (r: Z) (x: S) : iProp Σ
+    := sp_own (sp_i := rwlock_sp_inG) γ (Central e r x).
+Definition exc_pending γ : iProp Σ := sp_own (sp_i := rwlock_sp_inG) γ ExcPending.
+Definition exc_guard γ : iProp Σ := sp_own (sp_i := rwlock_sp_inG) γ ExcGuard.
+Definition sh_pending γ : iProp Σ := sp_own (sp_i := rwlock_sp_inG) γ ShPending.
+Definition sh_guard γ m : iProp Σ := sp_own (sp_i := rwlock_sp_inG) γ (ShGuard m).
 
 Definition rw_lock_inst (γ: gname) (f: S -> iProp Σ) : iProp Σ :=
-    @maps
-      (BaseOpt S) _ _ _ _ _ (RwLock S) _ _ _ _ _ _ _ _ _ Σ _ _
-    γ (base_opt_prop_map f).
+  sp_sto (sp_i := rwlock_sp_inG) γ (base_opt_prop_map f).
 
 (* Rw-Init *)
 
@@ -380,11 +372,11 @@ Lemma rw_new (x: S) (f: S -> iProp Σ) E
   : f x ={E}=∗ ∃ γ , rw_lock_inst γ f ∗ fields γ false 0 x.
 Proof. 
   iIntros "fx".
-  iMod (logic_init (Central false 0 x) (base_opt_prop_map f) E with "[fx]") as "x".
-  { apply rw_init_valid. }
+  iMod (sp_alloc (Central false 0 x) (Full x) (base_opt_prop_map f) E with "[fx]") as "x".
+  { split; trivial. apply rw_init_valid. }
   { apply wf_prop_base_base_opt. }
   {
-    unfold interp, rwlock_interp, Central, base_opt_prop_map. iFrame.
+    unfold sp_interp, rwlock_interp, Central, base_opt_prop_map. iFrame.
   }
   iDestruct "x" as (γ) "x". iModIntro. iExists γ.
   unfold rw_lock_inst, fields. iFrame.
@@ -394,11 +386,11 @@ Lemma rw_new_ns (x: S) (f: S -> iProp Σ) E (N: namespace)
   : f x ={E}=∗ ∃ γ , ⌜ γ ∈ (↑N : coPset) ⌝ ∗ rw_lock_inst γ f ∗ fields γ false 0 x.
 Proof. 
   iIntros "fx".
-  iMod (logic_init_ns (Central false 0 x) (base_opt_prop_map f) E N with "[fx]") as "x".
-  { apply rw_init_valid. }
+  iMod (sp_alloc_ns (Central false 0 x) (Full x) (base_opt_prop_map f) E N with "[fx]") as "x".
+  { split; trivial. apply rw_init_valid. }
   { apply wf_prop_base_base_opt. }
   {
-    unfold interp, rwlock_interp, Central, base_opt_prop_map. iFrame.
+    unfold sp_interp, rwlock_interp, Central, base_opt_prop_map. iFrame.
   }
   iDestruct "x" as (γ) "[%gn x]". iModIntro. iExists γ.
   iSplitL "". { iPureIntro. trivial. }
@@ -413,8 +405,8 @@ Lemma rw_exc_begin γ f rc (x: S) E
     fields γ false rc x ={ E }=∗ fields γ true rc x ∗ exc_pending γ.
 Proof.
   unfold fields, exc_pending.
-  rewrite <- p_own_op.
-  apply logic_update'; trivial.
+  rewrite <- sp_own_op.
+  apply sp_update'; trivial. rewrite eq_storage_protocol_update_ii.
   apply rw_mov_exc_begin.
 Qed.
 
@@ -428,11 +420,11 @@ Lemma rw_exc_acquire γ f exc (x: S) E
     fields γ exc 0 x ∗ exc_guard γ ∗ ▷ f x.
 Proof.
   unfold fields, exc_pending, exc_guard, rw_lock_inst.
-  rewrite <- p_own_op.
+  rewrite <- sp_own_op.
   rewrite <- bi.sep_assoc'.
-  rewrite <- p_own_op.
+  rewrite <- sp_own_op.
   replace (f x) with (base_opt_prop_map f (Full x)) by trivial.
-  apply logic_withdraw'; trivial.
+  apply sp_withdraw'; trivial. rewrite eq_storage_protocol_withdraw_ii.
   apply rw_mov_exc_acquire.
 Qed.
 
@@ -447,9 +439,9 @@ Lemma rw_exc_release γ f exc rc (x y: S) E
 Proof.
   unfold fields, exc_pending, exc_guard, rw_lock_inst.
   rewrite bi.sep_assoc.
-  rewrite <- p_own_op.
+  rewrite <- sp_own_op.
   replace (f x) with (base_opt_prop_map f (Full x)) by trivial.
-  apply logic_deposit'; trivial.
+  apply sp_deposit'; trivial. rewrite eq_storage_protocol_deposit_ii.
   apply rw_mov_exc_release.
 Qed.
 
@@ -463,8 +455,8 @@ Lemma rw_shared_begin γ f exc rc (x: S) E
       fields γ exc (rc+1) x ∗ sh_pending γ.
 Proof.
   unfold fields, sh_pending.
-  rewrite <- p_own_op.
-  apply logic_update'; trivial.
+  rewrite <- sp_own_op.
+  apply sp_update'; trivial. rewrite eq_storage_protocol_update_ii.
   apply rw_mov_shared_begin.
 Qed.
 
@@ -478,9 +470,9 @@ Lemma rw_shared_acquire γ f rc (x: S) E
       fields γ false rc x ∗ sh_guard γ x.
 Proof.
   unfold fields, sh_guard, sh_pending.
-  rewrite <- p_own_op.
-  rewrite <- p_own_op.
-  apply logic_update'; trivial.
+  rewrite <- sp_own_op.
+  rewrite <- sp_own_op.
+  apply sp_update'; trivial. rewrite eq_storage_protocol_update_ii.
   apply rw_mov_shared_acquire.
 Qed.
 
@@ -492,8 +484,8 @@ Lemma rw_shared_release γ f exc rc (x y: S) E
     fields γ exc rc x ∗ sh_guard γ y ={ E }=∗ fields γ exc (rc-1) x.
 Proof.
   unfold fields, sh_guard, sh_pending.
-  rewrite <- p_own_op.
-  apply logic_update'; trivial.
+  rewrite <- sp_own_op.
+  apply sp_update'; trivial. rewrite eq_storage_protocol_update_ii.
   apply rw_mov_shared_release.
 Qed.
 
@@ -505,8 +497,8 @@ Lemma rw_shared_retry γ f exc rc (x: S) E
     fields γ exc rc x ∗ sh_pending γ ={ E }=∗ fields γ exc (rc-1) x.
 Proof.
   unfold fields, sh_guard, sh_pending.
-  rewrite <- p_own_op.
-  apply logic_update'; trivial.
+  rewrite <- sp_own_op.
+  apply sp_update'; trivial. rewrite eq_storage_protocol_update_ii.
   apply rw_mov_shared_retry.
 Qed.
 
@@ -518,11 +510,9 @@ Lemma rw_borrow_back γ f (x: S)
 Proof.
   unfold sh_guard.
   replace (f x) with (base_opt_prop_map f (Full x)) by trivial.
-  apply logic_guard.
-  - apply rw_mov_shared_borrow.
+  apply sp_guard.
+  - rewrite eq_storage_protocol_guards_ii. apply rw_mov_shared_borrow.
   - set_solver.
 Qed.
 
 End RwlockLogic.
-
-
diff --git a/src/guarding/storage_protocol/base_storage_opt.v b/src/guarding/storage_protocol/base_storage_opt.v
index 239c00f..4b360e0 100644
--- a/src/guarding/storage_protocol/base_storage_opt.v
+++ b/src/guarding/storage_protocol/base_storage_opt.v
@@ -1,4 +1,3 @@
-Require Import guarding.storage_protocol.inved.
 Require Import guarding.storage_protocol.protocol.
 From iris.proofmode Require Import base ltac_tactics tactics coq_tactics reduction.
 
diff --git a/src/guarding/storage_protocol/protocol.v b/src/guarding/storage_protocol/protocol.v
index bf4c71f..5b41e18 100644
--- a/src/guarding/storage_protocol/protocol.v
+++ b/src/guarding/storage_protocol/protocol.v
@@ -11,145 +11,400 @@ From iris.proofmode Require Import coq_tactics.
 
 From stdpp Require Export namespaces.
 
-(*From iris.base_logic.lib Require Export wsat.*)
-
-Require Import guarding.storage_protocol.inved.
-Require Import guarding.guard.
+Require Import guarding.internal.inved.
 Require Import guarding.internal.auth_frag_util.
+Require Import guarding.internal.wsat_util.
+Require Import guarding.guard.
 Require Import guarding.factoring_props.
 Require Import guarding.own_and_own_sep.
-Require Import guarding.internal.wsat_util.
-
-(*
-Context {Σ: gFunctors}.
-Context `{!invGS Σ}.
-*)
+Require Import guarding.own_and.
 
-Class Interp (P : Type) (B : Type) := interp : P → B.
+Class SPRel (P : Type) (B : Type) := sp_rel : P → B → Prop.
 
+Class SPInv (P : Type) := sp_inv : P → Prop.
+Class SPInterp (P : Type) (B : Type) := sp_interp : P → B.
 
-Record StorageMixin P B
-    `{Equiv P, PCore P, Op P, Valid P, PInv P, Unit P}
-    {equ: @Equivalence P (≡)}
-    `{Equiv B, PCore B, Op B, Valid B, Unit B, Interp P B}
+Class StorageMixin P B
+    `{Equiv P, PCore P, Op P, Valid P, Unit P}
+    {equ_p: @Equivalence P (≡)}
+    `{Equiv B, PCore B, Op B, Valid B, Unit B, SPRel P B}
+    {equ_b: @Equivalence B (≡)}
 := {
-    protocol_mixin: ProtocolMixin P;
-    base_ra_mixin: RAMixin B; (* completely ignore core *)
+    protocol_ra_mixin: RAMixin P; (* ignore valid *)
+    base_ra_mixin: RAMixin B; (* ignore core *)
     
+    protocol_unit_left_id : LeftId equiv (ε : P) op;
     base_unit_left_id : LeftId equiv (ε : B) op;
 
-    interp_proper: Proper ((≡) ==> (≡)) interp;
-    interp_val: ∀ p: P , pinv p -> ✓ interp p;
+    sp_rel_proper: Proper ((≡) ==> (≡) ==> (↔)) sp_rel;
+    interp_val: ∀ (p: P) (b: B) , sp_rel p b → ✓ b;
 }. 
+Global Arguments protocol_ra_mixin (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments base_ra_mixin (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments protocol_unit_left_id (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments base_unit_left_id (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments sp_rel_proper (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments interp_val (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _} (_).
 
+Class StorageMixinII P B
+    `{Equiv P, PCore P, Op P, Valid P, Unit P}
+    {equ_p: @Equivalence P (≡)}
+    `{Equiv B, PCore B, Op B, Valid B, Unit B, SPInv P, SPInterp P B}
+    {equ_b: @Equivalence B (≡)}
+:= {
+    protocol_ra_mixin_ii: RAMixin P;
+    base_ra_mixin_ii: RAMixin B; (* completely ignore core *)
+    
+    protocol_unit_left_id_ii : LeftId equiv (ε : P) op;
+    base_unit_left_id_ii : LeftId equiv (ε : B) op;
+
+    sp_inv_proper_ii: Proper ((≡) ==> (↔)) sp_inv;
+    sp_interp_proper_ii: Proper ((≡) ==> (≡)) sp_interp;
+    interp_val_ii: ∀ (p: P) , sp_inv p → ✓ (sp_interp p);
+}.
+Global Arguments protocol_ra_mixin_ii (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments base_ra_mixin_ii (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments protocol_unit_left_id_ii (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments base_unit_left_id_ii (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments sp_inv_proper_ii (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments sp_interp_proper_ii (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _ _} (_).
+Global Arguments interp_val_ii (P B) {_ _ _ _ _ _ _ _ _ _ _ _ _ _} (_).
 
 Section PropMap.
   Context {Σ: gFunctors}.
-  
   Context `{Equiv B, Op B, Valid B, Unit B}.
   
-  Definition wf_prop_map (f: B -> iProp Σ) :=
+  Definition wf_prop_map (f: B → iProp Σ) :=
       Proper ((≡) ==> (≡)) f
-      /\ f ε ≡ (True)%I
-      /\ (∀ a b , ✓(a ⋅ b) -> f (a ⋅ b) ≡ (f a ∗ f b) % I).
-      
-  
+      ∧ f ε ≡ (True)%I
+      ∧ (∀ a b , ✓(a ⋅ b) → f (a ⋅ b) ≡ (f a ∗ f b) % I).
 End PropMap.
 
-Section StorageLogic.
+Section StorageRelations.
+  Context `{Equiv P, PCore P, Op P, Valid P, Unit P, SPRel P B}.
   Context `{Equiv B, PCore B, Op B, Valid B, Unit B}.
-  Context `{Equiv P, PCore P, Op P, PInv P, Valid P, Unit P, Interp P B}.
-  
   
   Definition storage_protocol_guards (p: P) (b: B) :=
-      ∀ q , pinv (p ⋅ q) -> b ≼ interp (p ⋅ q).
+      ∀ q (t: B) , sp_rel (p ⋅ q) t → b ≼ t.
       
   Definition storage_protocol_exchange (p1 p2: P) (b1 b2: B)  :=
-      ∀ q , pinv (p1 ⋅ q) -> pinv (p2 ⋅ q)
-          /\ ✓(interp (p1 ⋅ q) ⋅ b1)
-          /\ interp (p1 ⋅ q) ⋅ b1 ≡ interp (p2 ⋅ q) ⋅ b2.
+      ∀ q t1, sp_rel (p1 ⋅ q) t1 →
+          ∃ t2, sp_rel (p2 ⋅ q) t2
+          ∧ ✓(t1 ⋅ b1)
+          ∧ t1 ⋅ b1 ≡ t2 ⋅ b2.
           
   Definition storage_protocol_update (p1 p2: P) :=
-      ∀ q , pinv (p1 ⋅ q) -> pinv (p2 ⋅ q)
-          /\ interp (p1 ⋅ q) ≡ interp (p2 ⋅ q).
+      ∀ q t1 , sp_rel (p1 ⋅ q) t1 → sp_rel (p2 ⋅ q) t1.
           
   Definition storage_protocol_withdraw (p1 p2: P) (b2: B)  :=
-      ∀ q , pinv (p1 ⋅ q) -> pinv (p2 ⋅ q)
-          /\ interp (p1 ⋅ q) ≡ interp (p2 ⋅ q) ⋅ b2.
+      ∀ q t1 , sp_rel (p1 ⋅ q) t1 → ∃ t2, sp_rel (p2 ⋅ q) t2
+          ∧ t1 ≡ t2 ⋅ b2.
           
   Definition storage_protocol_deposit (p1 p2: P) (b1: B)  :=
-      ∀ q , pinv (p1 ⋅ q) -> pinv (p2 ⋅ q)
-          /\ ✓(interp (p1 ⋅ q) ⋅ b1)
-          /\ interp (p1 ⋅ q) ⋅ b1 ≡ interp (p2 ⋅ q).
+      ∀ q t1 , sp_rel (p1 ⋅ q) t1 → ∃ t2, sp_rel (p2 ⋅ q) t2
+          ∧ ✓(t1 ⋅ b1)
+          ∧ t1 ⋅ b1 ≡ t2.
           
-  Definition storage_protocol_exchange_nondeterministic (p1: P) (b1: B) (output_ok: P -> B -> Prop)  :=
-      ∀ q , pinv (p1 ⋅ q) -> ∃ p2 b2 , output_ok p2 b2
-          /\ pinv (p2 ⋅ q)
-          /\ ✓(interp (p1 ⋅ q) ⋅ b1)
-          /\ interp (p1 ⋅ q) ⋅ b1 ≡ interp (p2 ⋅ q) ⋅ b2.
+  Definition storage_protocol_exchange_nondeterministic (p1: P) (b1: B) (output_ok: P → B → Prop)  :=
+      ∀ q t1 , sp_rel (p1 ⋅ q) t1 → ∃ p2 b2 t2 , output_ok p2 b2
+          ∧ sp_rel (p2 ⋅ q) t2
+          ∧ ✓(t1 ⋅ b1)
+          ∧ t1 ⋅ b1 ≡ t2 ⋅ b2.
+End StorageRelations.
 
+Section StorageRelationsII.
+  Context {P B: Type}.
+  Context `{Equiv P, PCore P, Op P, Valid P, Unit P, SPInv P, SPInterp P B}.
+  Context `{Equiv B, PCore B, Op B, Valid B, Unit B}.
+  
+  Definition storage_protocol_guards_ii (p: P) (b: B) :=
+      ∀ q , sp_inv (p ⋅ q) → b ≼ sp_interp (p ⋅ q).
+      
+  Definition storage_protocol_exchange_ii (p1 p2: P) (b1 b2: B)  :=
+      ∀ q , sp_inv (p1 ⋅ q) → sp_inv (p2 ⋅ q)
+          ∧ ✓(sp_interp (p1 ⋅ q) ⋅ b1)
+          ∧ sp_interp (p1 ⋅ q) ⋅ b1 ≡ sp_interp (p2 ⋅ q) ⋅ b2.
+          
+  Definition storage_protocol_update_ii (p1 p2: P) :=
+      ∀ q , sp_inv (p1 ⋅ q) → sp_inv (p2 ⋅ q)
+          ∧ sp_interp (p1 ⋅ q) ≡ sp_interp (p2 ⋅ q).
+          
+  Definition storage_protocol_withdraw_ii (p1 p2: P) (b2: B)  :=
+      ∀ q , sp_inv (p1 ⋅ q) → sp_inv (p2 ⋅ q)
+          ∧ sp_interp (p1 ⋅ q) ≡ sp_interp (p2 ⋅ q) ⋅ b2.
+          
+  Definition storage_protocol_deposit_ii (p1 p2: P) (b1: B)  :=
+      ∀ q , sp_inv (p1 ⋅ q) → sp_inv (p2 ⋅ q)
+          ∧ ✓(sp_interp (p1 ⋅ q) ⋅ b1)
+          ∧ sp_interp (p1 ⋅ q) ⋅ b1 ≡ sp_interp (p2 ⋅ q).
           
-  Context {equ: Equivalence (≡@{P})}.
-  Context {equb: Equivalence (≡@{B})}.
-  Context {storage_mixin: StorageMixin P B}.
+  Definition storage_protocol_exchange_nondeterministic_ii (p1: P) (b1: B) (output_ok: P → B → Prop) :=
+      ∀ q , sp_inv (p1 ⋅ q) → ∃ p2 b2 , output_ok p2 b2
+          ∧ sp_inv (p2 ⋅ q)
+          ∧ ✓(sp_interp (p1 ⋅ q) ⋅ b1)
+          ∧ sp_interp (p1 ⋅ q) ⋅ b1 ≡ sp_interp (p2 ⋅ q) ⋅ b2.
+End StorageRelationsII.
+
+Section StorageRelationsIILemmas.
+  Context `{Equiv B, PCore B, Op B, Valid B, Unit B}.
+  Context `{Equiv P, PCore P, Op P, Valid P, Unit P, SPInv P, SPInterp P B}.
+  Context {equ_p: @Equivalence P (≡)}.
+  Context {equ_b: @Equivalence B (≡)}.
+  Context {storage_mixin_ii: StorageMixinII P B}.
+  
+  Global Instance sp_rel_of_ii : SPRel P B := λ p b , sp_inv p ∧ sp_interp p ≡ b.
+          
+  Local Instance base_ra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op B _).
+  Proof using storage_mixin_ii.
+    unfold Proper, "==>". intros x y Heq x0 y0 Heq0.
+    enough (x ⋅ x0 ≡ y ⋅ x0) as X.
+    { setoid_rewrite X.
+      eapply (ra_op_proper _ (base_ra_mixin_ii _ _ storage_mixin_ii)). trivial. }
+    setoid_rewrite (ra_comm _ (base_ra_mixin_ii _ _ storage_mixin_ii) x x0).
+    setoid_rewrite (ra_comm _ (base_ra_mixin_ii _ _ storage_mixin_ii) y x0).
+    eapply (ra_op_proper _ (base_ra_mixin_ii _ _ storage_mixin_ii)). trivial.
+  Qed.
+  
+  Local Instance base_ra_valid_proper : Proper ((≡) ==> (↔)) (@valid B _).
+  Proof using storage_mixin_ii.
+    unfold Proper, "==>". intros x y Heq. split.
+    - intros Hval. eapply (ra_validN_proper _ (base_ra_mixin_ii _ _ storage_mixin_ii)).
+        { eapply Heq. } apply Hval.
+    - intros Hval. eapply (ra_validN_proper _ (base_ra_mixin_ii _ _ storage_mixin_ii)).
+        { symmetry. eapply Heq. } apply Hval.
+  Qed.
+  
+  Lemma eq_storage_protocol_guards_ii (p: P) (b: B)
+    : storage_protocol_guards p b ↔ storage_protocol_guards_ii p b.
+  Proof using equ_b.
+    unfold storage_protocol_guards, storage_protocol_guards_ii. split.
+    - intros Q q spi. apply (Q q). split; trivial.
+    - intros Q q t [Hi Heq]. destruct (Q q Hi) as [z Hj]. exists z.
+      setoid_rewrite <- Heq. trivial.
+  Qed.
+   
+  Lemma eq_storage_protocol_exchange_ii (p1 p2: P) (b1 b2: B)
+    : storage_protocol_exchange p1 p2 b1 b2 ↔ storage_protocol_exchange_ii p1 p2 b1 b2.
+  Proof using storage_mixin_ii.
+    unfold storage_protocol_exchange, storage_protocol_exchange_ii. split.
+    - intros Q q Hspi. destruct (Q q (sp_interp (p1 ⋅ q))) as [b [[Hbi Hbin] [Hc1 Hceq]]].
+      + split; trivial.
+      + split; trivial. split; trivial. setoid_rewrite Hbin. trivial.
+    - intros Q q t1 [Hspi Heq]. exists (sp_interp (p2 ⋅ q)).
+      destruct (Q q Hspi) as [Hspi2 [Hval Heq2]]. split; trivial.
+      + split; trivial.
+      + split; trivial.
+        * setoid_rewrite <- Heq; trivial.
+        * setoid_rewrite <- Heq; trivial.
+  Qed.
+  
+  Lemma eq_storage_protocol_update_ii (p1 p2: P)
+    : storage_protocol_update p1 p2 ↔ storage_protocol_update_ii p1 p2.
+  Proof using equ_b.
+    unfold storage_protocol_update, storage_protocol_update_ii. split.
+    - intros Q q Hspi. destruct (Q q (sp_interp (p1 ⋅ q))) as [b Hb].
+      + split; trivial.
+      + split; trivial.
+    - intros Q q t1 [Hspi Heq].
+      destruct (Q q Hspi) as [Hspi2 Heq2]. split; trivial.
+      + setoid_rewrite <- Heq2. trivial.
+  Qed.
+  
+  Lemma eq_storage_protocol_withdraw_ii (p1 p2: P) (b2: B)
+    : storage_protocol_withdraw p1 p2 b2 ↔ storage_protocol_withdraw_ii p1 p2 b2.
+  Proof using storage_mixin_ii.
+    unfold storage_protocol_withdraw, storage_protocol_withdraw_ii. split.
+    - intros Q q Hspi. destruct (Q q (sp_interp (p1 ⋅ q))) as [b [[Hba Hbb] Hc]].
+      + split; trivial.
+      + split; trivial. setoid_rewrite Hbb. trivial.
+    - intros Q q t1 [Hspi Heq]. exists (sp_interp (p2 ⋅ q)).
+      destruct (Q q Hspi) as [Hspi2 Heq2]. split; trivial.
+      + split; trivial.
+      + setoid_rewrite <- Heq. trivial.
+  Qed.
+  
+  Lemma eq_storage_protocol_deposit_ii (p1 p2: P) (b1: B)
+    : storage_protocol_deposit p1 p2 b1 ↔ storage_protocol_deposit_ii p1 p2 b1.
+  Proof using storage_mixin_ii.
+    unfold storage_protocol_deposit, storage_protocol_deposit_ii. split.
+    - intros Q q Hspi. destruct (Q q (sp_interp (p1 ⋅ q))) as [b [[Hbi Hbin] [Hc1 Hceq]]].
+      + split; trivial.
+      + split; trivial. split; trivial. setoid_rewrite Hbin. trivial.
+    - intros Q q t1 [Hspi Heq]. exists (sp_interp (p2 ⋅ q)).
+      destruct (Q q Hspi) as [Hspi2 [Hval Heq2]]. split; trivial.
+      + split; trivial.
+      + split; trivial.
+        * setoid_rewrite <- Heq; trivial.
+        * setoid_rewrite <- Heq; trivial.
+  Qed.
+  
+  Lemma eq_storage_protocol_exchange_nondeterministic_ii (p1: P) (b1: B) (output_ok: P → B → Prop)
+    : storage_protocol_exchange_nondeterministic p1 b1 output_ok
+      ↔ storage_protocol_exchange_nondeterministic_ii p1 b1 output_ok.
+  Proof using storage_mixin_ii.
+    unfold storage_protocol_exchange_nondeterministic,
+      storage_protocol_exchange_nondeterministic_ii. split.
+     - intros Q q Hspi.
+        destruct (Q q (sp_interp (p1 ⋅ q))) as [p2 [b2 [t2 [Hoo [Hrel [Hval Heq]]]]]].
+      + split; trivial.
+      + destruct Hrel as [Ha Hb]. exists p2. exists b2. split; trivial. split; trivial.
+        split; trivial. setoid_rewrite Hb. trivial.
+     - intros Q q t1 [Hinv Hint]. destruct (Q q Hinv) as [p2 [b2 [Hoo [Hspinv [Hval Heq]]]]].
+        exists p2. exists b2. exists (sp_interp (p2 ⋅ q)). split; trivial.
+        split.
+        + split; trivial.
+        + split.
+          * setoid_rewrite <- Hint. trivial.
+          * setoid_rewrite <- Hint. trivial.
+  Qed.
+End StorageRelationsIILemmas.
 
-  Instance sm_interp_proper
-      : Proper ((≡) ==> (≡)) (interp).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ storage_mixin.
+Global Instance storage_mixin_from_ii
+  `{Equiv B, PCore B, Op B, Valid B, Unit B}
+  `{Equiv P, PCore P, Op P, Valid P, Unit P, SPInv P, SPInterp P B}
+  {equ_p: @Equivalence P (≡)}
+  {equ_b: @Equivalence B (≡)}
+  (storage_mixin_ii: StorageMixinII P B) : StorageMixin P B.
+Proof.
+    split.
+     - apply (protocol_ra_mixin_ii P B storage_mixin_ii).
+     - apply (base_ra_mixin_ii P B storage_mixin_ii).
+     - apply (protocol_unit_left_id_ii P B storage_mixin_ii).
+     - apply (base_unit_left_id_ii P B storage_mixin_ii).
+     - intros x y Heq x0 y0 Heq0. split.
+        + intros [Hinv HeqX]. split.
+          * rewrite (sp_inv_proper_ii _ _ storage_mixin_ii). { apply Hinv. } symmetry.
+              apply Heq.
+          * setoid_rewrite Heq0 in HeqX.
+            rewrite (sp_interp_proper_ii _ _ storage_mixin_ii). { apply HeqX. }
+            symmetry. apply Heq.
+        + intros [Hinv HeqX]. split.
+          * rewrite (sp_inv_proper_ii _ _ storage_mixin_ii). { apply Hinv. }
+              apply Heq.
+          * setoid_rewrite <- Heq0 in HeqX.
+            rewrite (sp_interp_proper_ii _ _ storage_mixin_ii). { apply HeqX. }
+            apply Heq.
+     - intros p b [Ha Hb]. rewrite base_ra_valid_proper. 
+      { apply (interp_val_ii _ _ storage_mixin_ii). apply Ha. } { trivial. }
+Qed.
+
+Local Instance sp_rel_pinv {P B : Type} {ir: SPRel P B} : InternalPInv P :=
+  λ p , ∃ b , sp_rel p b.
+  
+Local Definition internal_protocol_mixin_storage_mixin
+    `{Equiv P, PCore P, Op P, Valid P, Unit P}
+    {equ_p: @Equivalence P (≡)}
+    `{Equiv B, PCore B, Op B, Valid B, Unit B, SPRel P B}
+    {equ_b: @Equivalence B (≡)}
+    (storage_mixin: StorageMixin P B)
+    : InternalProtocolMixin P.
+Proof.
+  destruct storage_mixin as [Q1 Q2 Q3 Q4 irp Q5]. split; trivial.
+  unfold Proper, "==>", impl. intros x y Heq. unfold pinv, sp_rel_pinv.
+  intros [b J]. unfold Proper, "==>", impl in irp.
+  setoid_rewrite (irp x y _ b b) in J; trivial. exists b. trivial.
+Qed.
+
+Class sp_logicG
+    `{Equiv P, PCore P, Op P, Valid P, Unit P} `{equ_p: @Equivalence P (≡)}
+    `{Equiv B, PCore B, Op B, Valid B, Unit B, SPRel P B} `{equ_b: @Equivalence B (≡)}
+    (storage_mixin: StorageMixin P B) Σ
+:= {
+  #[local] sp_authG :: inG Σ (authUR (inved_protocolUR
+                          (internal_protocol_mixin_storage_mixin storage_mixin)))
+}.
+
+Definition sp_logicΣ
+    `{Equiv P, PCore P, Op P, Valid P, Unit P} `{equ_p: @Equivalence P (≡)}
+    `{Equiv B, PCore B, Op B, Valid B, Unit B, SPRel P B} `{equ_b: @Equivalence B (≡)}
+    (storage_mixin: StorageMixin P B)
+: gFunctors := #[
+  GFunctor (authUR (inved_protocolUR
+                          (internal_protocol_mixin_storage_mixin storage_mixin)))
+].
+
+Global Instance subG_sp_logicΣ
+  `{Equiv P, PCore P, Op P, Valid P, Unit P} `{equ_p: @Equivalence P (≡)}
+  `{Equiv B, PCore B, Op B, Valid B, Unit B, SPRel P B} `{equ_b: @Equivalence B (≡)}
+  (storage_mixin: StorageMixin P B) Σ
+    : subG (sp_logicΣ storage_mixin) Σ → sp_logicG storage_mixin Σ.
+Proof.
+  solve_inG.
+Qed.
+
+Section StorageLogic.
+  Context {P B : Type}.
+  Context `{Equiv P, PCore P, Op P, Valid P, HPUnit: Unit P, SPRel P B}.
+  Context `{Equiv B, PCore B, Op B, Valid B, Unit B}.
+  Context `{equ_p: @Equivalence P (≡)}.
+  Context `{equ_b: @Equivalence B (≡)}.
+  Context `{storage_mixin: !StorageMixin P B}.
+
+  Local Instance sm_interp_proper
+      : Proper ((≡) ==> (≡) ==> (↔)) (sp_rel).
+  Proof using storage_mixin.
     destruct storage_mixin. trivial.
   Qed.
+  
+  Local Instance sm_pinv_proper
+      : Proper ((≡) ==> (↔)) (@pinv P sp_rel_pinv).
+  Proof using storage_mixin.
+    unfold Proper, "==>", pinv. intros x y Heq. split.
+    -  unfold sp_rel_pinv. intros [b Hx]. exists b. setoid_rewrite <- Heq. trivial.
+    -  unfold sp_rel_pinv. intros [b Hy]. exists b. setoid_rewrite Heq. trivial.
+  Qed.
 
-  Instance inved_proper
+  Local Instance inved_proper
       : Proper ((≡) ==> (≡)) (@Inved P).
   Proof.
     unfold Proper, "==>". intros.
     unfold "≡", inved_protocol_equiv. trivial.
   Qed.
                    
-  Global Instance my_discrete : CmraDiscrete (inved_protocolR (protocol_mixin P B storage_mixin)).
+  Global Instance my_discrete : CmraDiscrete (inved_protocolR (internal_protocol_mixin_storage_mixin storage_mixin)).
   Proof. apply discrete_cmra_discrete. Qed.
 
   Context {Σ: gFunctors}.
-  Context `{!inG Σ (authUR (inved_protocolUR (protocol_mixin P B storage_mixin)))}.
+  Context `{sp_i: !sp_logicG storage_mixin Σ}.
   Context `{!invGS Σ}.
   
-  Definition maps (γ: gname) (f: B -> iProp Σ) : iProp Σ :=
+  Definition sp_sto (γ: gname) (f: B → iProp Σ) : iProp Σ :=
       ⌜ wf_prop_map f ⌝ ∗
       own γ (◯ (Inved ε)) ∗
       ownI γ (
-        ∃ (state: P) ,
-          own γ (● (Inved state))
-          ∗ ⌜ pinv state ⌝
-          ∗ (f (interp state))
+        ∃ (state_t: P * B) ,
+          own γ (● (Inved (fst state_t)))
+          ∗ ⌜ sp_rel (fst state_t) (snd state_t) ⌝
+          ∗ (f (snd state_t))
       ). 
      
-  Definition p_own (γ: gname) (p: P) : iProp Σ := own γ (◯ (Inved p)).
+  Local Definition sp_own_def (γ: gname) (p: P) : iProp Σ := own γ (◯ (Inved p)).
+  Local Definition sp_own_aux : seal (@sp_own_def). Proof. by eexists. Qed.
+  Definition sp_own := sp_own_aux.(unseal).
+  Local Definition sp_own_eq : @sp_own = @sp_own_def := sp_own_aux.(seal_eq).
   
   Lemma pcore_inved_unit
     : (pcore (Inved (ε : P)) ≡ Some (Inved ε)).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    unfold pcore, inved_protocol_pcore. destruct (pcore ε) eqn:x.
-    { destruct storage_mixin. destruct protocol_mixin0. destruct protocol_ra_mixin.
-      have k := ra_pcore_l (ε: P) p x.
-      generalize k. rewrite ra_comm. rewrite protocol_unit_left_id.
+  Proof using equ_p storage_mixin.
+    unfold pcore, inved_protocol_pcore. destruct (pcore ε) as [p|] eqn:x.
+    {
+      have p_ra_mixin := (protocol_ra_mixin _ _ storage_mixin).
+      have k := ra_pcore_l _ p_ra_mixin (ε: P) p x.
+      generalize k. rewrite ra_comm; trivial. rewrite protocol_unit_left_id; trivial.
       intro R. setoid_rewrite R. trivial.
     }
     trivial.
   Qed.
   
-  Global Instance pers_own_frag_inved_unit γ : Persistent (own γ (◯ (Inved (ε: P)))).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    apply own_core_persistent.
-    apply auth_frag_core_id.
-    unfold CoreId.
-    apply pcore_inved_unit.
+  Local Instance pers_own_frag_inved_unit γ : Persistent (own γ (◯ (Inved (ε: P)))).
+  Proof using equ_p.
+    apply own_core_persistent. apply auth_frag_core_id. unfold CoreId. apply pcore_inved_unit.
   Qed.
   
-  Global Instance pers_maps γ f : Persistent (maps γ f).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-  apply _. Qed.
-  
-  Lemma apply_timeless (X Y Z W V : iProp Σ) (ti: Timeless Z) (ti2: Timeless W)
+  Global Instance pers_sto γ f : Persistent (sp_sto γ f).
+  Proof using equ_p. apply _. Qed.
+   
+  Lemma apply_timeless_rhs4 (X Y Z W V : iProp Σ) (ti: Timeless Z) (ti2: Timeless W)
       : X ∧ (Y ∗ ▷ (Z ∗ W ∗ V)) -∗ ◇ (X ∧ (Y ∗ Z ∗ W ∗ ▷ (V))).
   Proof.
       iIntros "l".
@@ -161,7 +416,7 @@ Section StorageLogic.
       iModIntro. iFrame.
   Qed.
   
-  Lemma stuff1 (X Y Z W V : iProp Σ)
+  Lemma and_rhs3_entails (X Y Z W V : iProp Σ)
       : (X ∧ (Y ∗ Z ∗ W ∗ V)) ⊢ W.
   Proof.
     iIntros "x". iDestruct "x" as "[_ [_ [_ [w _]]]]". iFrame.
@@ -171,19 +426,15 @@ Section StorageLogic.
     (incll :
       @included (InvedProtocol P) (inved_protocol_equiv P) (inved_protocol_op P)
       (Inved p1) (Inved p2)) : p1 ≼ p2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
+  Proof using storage_mixin.
     unfold "≼" in incll. destruct incll as [z incll].
-    destruct z.
+    destruct z as [|p].
     - unfold "⋅", inved_protocol_op, "≡", inved_protocol_equiv in incll.
       unfold "≼". exists ε.
       setoid_rewrite (@comm P).
-      + destruct storage_mixin. destruct protocol_mixin0.
-          setoid_rewrite incll.
-          unfold LeftId in protocol_unit_left_id.
-          symmetry.
-          apply protocol_unit_left_id.
-      + destruct storage_mixin. destruct protocol_mixin0. destruct protocol_ra_mixin.
-          apply ra_comm.
+      + setoid_rewrite incll.
+        setoid_rewrite protocol_unit_left_id; trivial. apply storage_mixin.
+      + apply (ra_comm _ (protocol_ra_mixin _ _ storage_mixin)).
    - unfold "≡", inved_protocol_equiv, "⋅", inved_protocol_op in incll.
       unfold "≼". exists p. trivial.
   Qed.
@@ -204,29 +455,29 @@ Section StorageLogic.
   
   (* SP-Guard *)
   
-  Lemma logic_guard (p: P) (b: B) (γ: gname) (E: coPset) (f: B -> iProp Σ)
+  Lemma sp_guard (p: P) (b: B) (γ: gname) (E: coPset) (f: B → iProp Σ)
     (g: storage_protocol_guards p b)
     (is_in: γ ∈ E)
-    : maps γ f ⊢ (p_own γ p &&{ E }&&> ▷ f b).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps. iIntros "[%wfm [#ounit #oinv]]".
+    : sp_sto γ f ⊢ (sp_own γ p &&{ E }&&> ▷ f b).
+  Proof using equ_p.
+    unfold sp_sto. iIntros "[%wfm [#ounit #oinv]]".
     iDestruct (guards_from_inv _ _ E with "oinv") as "mg". { set_solver. }
-    assert (Inhabited P) as IP. { apply populate. apply ε. }
+    assert (Inhabited (P * B)) as IP. { apply populate. apply (ε, ε). }
     rewrite bi.later_exist.
-    iDestruct (guards_true E (p_own γ p)) as "gt".
-    iDestruct (guards_transitive _ (p_own γ p) True%I with "[gt mg]") as "gg".
+    iDestruct (guards_true E (sp_own γ p)) as "gt".
+    iDestruct (guards_transitive _ (sp_own γ p) True%I with "[gt mg]") as "gg".
       { iFrame "gt". iFrame "mg". }
-    iDestruct (lguards_exists_with_lhs P (p_own γ p) 
-      (λ state: P, (▷ (⌜ p ≼ state ⌝))%I)
-      (λ state: P, (▷ (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)))%I)
+    iDestruct (lguards_exists_with_lhs (P*B) (sp_own γ p) 
+      (λ (state_t: P*B), (▷ (⌜ p ≼ state_t.1 ⌝))%I)
+      (λ (state_t: P*B), (▷ (own γ (● Inved state_t.1) ∗ ⌜sp_rel state_t.1 state_t.2⌝ ∗ f state_t.2))%I)
       E 0
       with "[gg]") as "ggg".
     {
-      iIntros (x) "o". unfold p_own. iNext. iDestruct (auth_frag_conjunct_to_incl with "o") as "o"; trivial.
+      iIntros (x) "o". rewrite sp_own_eq. unfold sp_own_def. iNext. iDestruct (auth_frag_conjunct_to_incl with "o") as "o"; trivial.
     }
     { unfold guards. iFrame "gg". }
-    assert ((∃ x, ▷ (own γ (● Inved x) ∗ ⌜pinv x⌝ ∗ f (interp x)) ∗ ▷ ⌜p ≼ x⌝)
-      ⊣⊢ (▷ f b ∗ ▷(f b -∗ ∃ x, (own γ (● Inved x) ∗ ⌜pinv x⌝ ∗ f (interp x)) ∗ ⌜p ≼ x⌝)))
+    assert ((∃ x, ▷ (own γ (● Inved x.1) ∗ ⌜sp_rel x.1 x.2⌝ ∗ f x.2) ∗ ▷ ⌜p ≼ x.1⌝)
+      ⊣⊢ (▷ f b ∗ ▷(f b -∗ ∃ x, (own γ (● Inved x.1) ∗ ⌜sp_rel x.1 x.2⌝ ∗ f x.2) ∗ ⌜p ≼ x.1⌝)))
       as Equ.
     { iIntros. iSplit. { iIntros "r".
       rewrite <- bi.later_sep. iNext.
@@ -234,23 +485,20 @@ Section StorageLogic.
       unfold storage_protocol_guards in g.
       have p_incl_x_copy := p_incl_x.
       unfold "≼" in p_incl_x. destruct p_incl_x as [z p_incl_x].
-      assert (pinv (p ⋅ z)) as pinv_pz.
-          { destruct storage_mixin. destruct protocol_mixin0. setoid_rewrite <- p_incl_x. trivial. }
-      have b_le_interp := g z pinv_pz.
+      assert (sp_rel (p ⋅ z) state.2) as pinv_pz.
+          { setoid_rewrite <- p_incl_x. trivial. }
+      have b_le_interp := g z (state.2) pinv_pz.
       destruct b_le_interp as [bz b_le_interp].
       
-      assert (interp state ≡ b ⋅ bz) as ieqop.
-      { destruct storage_mixin. unfold interp. 
-          setoid_rewrite p_incl_x. trivial. }
-
       unfold wf_prop_map in wfm.
       destruct wfm as [fprop [funit fop]].
 
       assert (✓ (b ⋅ bz)) as is_val.
-      { destruct storage_mixin. destruct base_ra_mixin0.
-          setoid_rewrite <- ieqop. apply interp_val0. trivial. }
+      { destruct (base_ra_mixin _ _ storage_mixin).
+          setoid_rewrite <- b_le_interp.
+          apply (interp_val _ _ storage_mixin) with (p := p ⋅ z). trivial. }
           
-      setoid_rewrite ieqop.
+      setoid_rewrite b_le_interp.
       setoid_rewrite fop; trivial.
 
       iDestruct "t" as "[fb fbz]".
@@ -258,9 +506,11 @@ Section StorageLogic.
       iIntros "fb".
       iExists state.
       
-      setoid_rewrite ieqop.
+      setoid_rewrite b_le_interp.
       setoid_rewrite fop; trivial.
       iFrame. iSplit; iPureIntro; trivial.
+      setoid_rewrite p_incl_x. setoid_rewrite <- b_le_interp.
+      trivial.
     }
     { iIntros "[a b]". 
       iDestruct ("b" with "a") as "b".
@@ -272,13 +522,13 @@ Section StorageLogic.
     iApply guards_weaken_rhs_l. iFrame "ggg".
   Qed.
    
-  Lemma own_sep_inv_incll_helper_nondet (p1 st : P) (output_ok : P -> P -> Prop)
-    (cond : ∀ q : P, pinv (p1 ⋅ q) → ∃ p2 , output_ok p2 q /\ pinv (p2 ⋅ q))
-   : ∀ (z: InvedProtocol P) , pinv st -> ✓ (Inved st) -> Inved p1 ⋅ z ≡ Inved st →
-    ∃ p2 , output_ok p2 (match z with Inved z0 => z0 | Nah => ε end) /\ ✓ (Inved p2 ⋅ z).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
+  Lemma own_sep_inv_incll_helper_nondet (p1 st : P) (t1 : B) (output_ok : P → P → Prop)
+    (cond : ∀ (q : P) , sp_rel (p1 ⋅ q) t1 → ∃ p2 t2 , output_ok p2 q ∧ sp_rel (p2 ⋅ q) t2)
+   : ∀ (z: InvedProtocol P) , sp_rel st t1 → ✓ (Inved st) → Inved p1 ⋅ z ≡ Inved st →
+    ∃ p2 , output_ok p2 (match z with Inved z0 => z0 | Nah => ε end) ∧ ✓ (Inved p2 ⋅ z).
+  Proof using storage_mixin.
   intros z inv v eq.
-    destruct z.
+    destruct z as [|p].
     - unfold "⋅", inved_protocol_op.
       unfold "⋅", inved_protocol_op in eq.
       unfold "≡", inved_protocol_equiv in eq.
@@ -288,28 +538,24 @@ Section StorageLogic.
       {
         unfold "✓", inved_protocol_valid in v. 
         destruct v as [v pi].
-        assert (p1 ⋅ (@ε _ H9) ≡ p1) as eq2.
-        { destruct storage_mixin. destruct protocol_mixin0.
-            destruct protocol_ra_mixin.
-            rewrite ra_comm.
-            apply protocol_unit_left_id.
+        assert (p1 ⋅ (@ε _ HPUnit) ≡ p1) as eq2.
+        { 
+            rewrite (ra_comm _ (protocol_ra_mixin _ _ storage_mixin)).
+            apply (protocol_unit_left_id P B storage_mixin).
         }
-        assert (pinv (p1 ⋅ (@ε _ H9))) as pi2.
+        assert (sp_rel (p1 ⋅ (@ε _ HPUnit)) t1) as pi2.
         {
-          destruct storage_mixin.
-          destruct protocol_mixin0.
-          unfold Proper, "==>", impl in inv_proper.
-          apply inv_proper with (x := p1); trivial.
-          apply inv_proper with (x := st); trivial.
+          setoid_rewrite eq2. setoid_rewrite eq. trivial.
         }
-        have c := cond (@ε _ H9) pi2.
-        destruct c as [p2 [oo c]].
+        have c := cond (@ε _ HPUnit) pi2.
+        destruct c as [p2 [b [oo c]]].
         exists p2.
         split. { apply oo. }
         exists ε.
         trivial.
+        unfold pinv, sp_rel_pinv. exists b. apply c.
       }
-      { destruct storage_mixin. trivial. }
+      { apply (internal_protocol_mixin_storage_mixin storage_mixin). }
     - unfold "⋅", inved_protocol_op in eq.
       unfold "≡", inved_protocol_equiv in eq.
       unfold "⋅", inved_protocol_op.
@@ -320,152 +566,40 @@ Section StorageLogic.
         unfold "✓", inved_protocol_valid.
         destruct v as [v pi].
         
-        assert (pinv (p1 ⋅ p)) as pinv1. {
-          destruct storage_mixin.
-          destruct protocol_mixin0.
-          unfold Proper, "==>", impl in inv_proper.
-          apply inv_proper with (x := p1 ⋅ p); trivial.
-          apply inv_proper with (x := st); trivial.
+        assert (sp_rel (p1 ⋅ p) t1) as pinv1. {
+          setoid_rewrite eq. trivial.
         }
         have c := cond p pinv1.
-        destruct c as [p2 [oo c]].
+        destruct c as [p2 [b [oo c]]].
         exists p2.
         split; trivial.
         exists ε.
         
-        destruct storage_mixin.
-        destruct protocol_mixin0.
-        unfold Proper, "==>", impl in inv_proper.
-        assert (p2 ⋅ p ⋅ (@ε _ H9) ≡ p2 ⋅ p) as eq2.
-        { destruct storage_mixin. destruct protocol_mixin0.
-            destruct protocol_ra_mixin.
-            rewrite ra_comm.
-            apply protocol_unit_left_id.
+        assert (p2 ⋅ p ⋅ (@ε _ HPUnit) ≡ p2 ⋅ p) as eq2.
+        { 
+            rewrite (ra_comm _ (protocol_ra_mixin _ _ storage_mixin)).
+            apply (protocol_unit_left_id _ _ storage_mixin).
         }
-        apply inv_proper with (x := p2 ⋅ p); trivial.
+        setoid_rewrite eq2. exists b. trivial.
       }
-      { destruct storage_mixin. trivial. }
+      { apply (internal_protocol_mixin_storage_mixin storage_mixin). }
   Qed.
   
-  (*
-  Lemma own_sep_inv_incll_helper (p1 p2 st : P)
-    (cond : ∀ q : P, pinv (p1 ⋅ q) → pinv (p2 ⋅ q))
-   : ∀ (z: InvedProtocol P) , ✓ (Inved st) -> Inved p1 ⋅ z ≡ Inved st → ✓ (Inved p2 ⋅ z).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    intros z v eq.
-    destruct z.
-    - unfold "⋅", inved_protocol_op.
-      unfold "⋅", inved_protocol_op in eq.
-      unfold "≡", inved_protocol_equiv in eq.
-      unfold "✓", inved_protocol_valid. 
-      
-      setoid_rewrite <- eq in v.
-      {
-        unfold "✓", inved_protocol_valid in v. 
-        destruct v as [v pi].
-        have c := cond v pi.
-        exists v.
-        trivial.
-      }
-      { destruct storage_mixin. trivial. }
-    - unfold "⋅", inved_protocol_op in eq.
-      unfold "≡", inved_protocol_equiv in eq.
-      unfold "⋅", inved_protocol_op.
-      
-      setoid_rewrite <- eq in v.
-      {
-        unfold "✓", inved_protocol_valid in v.
-        unfold "✓", inved_protocol_valid.
-        destruct v as [v pi].
-        
-        assert (pinv (p1 ⋅ (p ⋅ v))) as pinv1. {
-          destruct storage_mixin.
-          destruct protocol_mixin0.
-          unfold Proper, "==>", impl in inv_proper.
-          apply inv_proper with (x := p1 ⋅ p ⋅ v); trivial.
-          destruct protocol_ra_mixin.
-          symmetry.
-          apply ra_assoc.
-        }
-        have c := cond (p ⋅ v) pinv1.
-        exists v.
-        
-        destruct storage_mixin.
-        destruct protocol_mixin0.
-        unfold Proper, "==>", impl in inv_proper.
-        apply inv_proper with (x := p2 ⋅ (p ⋅ v)); trivial.
-        destruct protocol_ra_mixin.
-        apply ra_assoc.
-      }
-      { destruct storage_mixin. trivial. }
-  Qed.
-  *)
-        
   Lemma op_nah (p1 state : P)
-    : Inved p1 ⋅ Nah ≡ Inved state -> p1 ≡ state.
+    : Inved p1 ⋅ Nah ≡ Inved state → p1 ≡ state.
   Proof. intros. trivial. Qed.
   
   Lemma op_inved_inved (p1 p2 p : P)
-    : Inved p1 ⋅ Inved p2 ≡ Inved p -> p1 ⋅ p2 ≡ p.
+    : Inved p1 ⋅ Inved p2 ≡ Inved p → p1 ⋅ p2 ≡ p.
   Proof. intros. trivial. Qed.
         
-  (*
-  Lemma own_sep_inv_incll γ (p1 p2 state : P)
-      (cond: ∀ q , pinv (p1 ⋅ q) -> pinv (p2 ⋅ q))
-    : own γ (◯ Inved p1) ∗ own γ (● Inved state) ==∗
-      ∃ (z: P) , ⌜ state ≡ p1 ⋅ z ⌝ ∗ own γ (◯ Inved p2) ∗ own γ (● Inved (p2 ⋅ z)).
-  Proof.
-    iIntros "[x y]".
-    iDestruct (own_valid with "y") as "%val".
-    iMod (own_sep_auth_incll γ (Inved p1) (Inved p2) (Inved state) with "[x y]") as "x".
-    {
-      intro.
-      apply own_sep_inv_incll_helper; trivial.
-      generalize val. rewrite auth_auth_valid. trivial.
-    }
-    { iFrame. }
-    iDestruct "x" as (z) "[%eq [frag auth]]".
-    destruct z.
-    {
-      have eq0 := op_nah _ _ eq.
-      assert (Inved p2 ⋅ Nah ≡ Inved p2) as eq1 by trivial.
-      setoid_rewrite eq1.
-      iExists (ε:P).
-      assert (p2 ⋅ ε ≡ p2) as eq2.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
-      }
-      setoid_rewrite eq2.
-      iFrame.
-      iPureIntro.
-      assert (p1 ⋅ ε ≡ p1) as eq3.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
-      }
-      setoid_rewrite eq3. symmetry. trivial.
-    }
-    {
-      iExists p.
-      
-      assert (Inved p2 ⋅ Inved p ≡ Inved (p2 ⋅ p)) as eq0 by trivial.
-      setoid_rewrite eq0.
-      iFrame.
-      iPureIntro. symmetry. apply op_inved_inved. trivial.
-    }
-   Qed.
-   *)
-   
-   Lemma own_sep_inv_incll_nondet γ (p1 state : P) (output_ok: P -> P -> Prop)
-      (cond: ∀ q , pinv (p1 ⋅ q) -> ∃ p2 , output_ok p2 q /\ pinv (p2 ⋅ q))
-      (pi: pinv state)
+  Lemma own_sep_inv_incll_nondet γ (p1 state : P) (t1: B) (output_ok: P → P → Prop)
+      (cond: ∀ q , sp_rel (p1 ⋅ q) t1 → ∃ p2 t2 , output_ok p2 q ∧ sp_rel (p2 ⋅ q) t2)
+      (pi: sp_rel state t1)
     : own γ (◯ Inved p1) ∗ own γ (● Inved state) ==∗
-      ∃ (z p2: P) , ⌜ output_ok p2 z /\ state ≡ p1 ⋅ z ⌝
+      ∃ (z p2: P) , ⌜ output_ok p2 z ∧ state ≡ p1 ⋅ z ⌝
           ∗ own γ (◯ Inved p2) ∗ own γ (● Inved (p2 ⋅ z)).
-   Proof.
+  Proof using storage_mixin.
    iIntros "[x y]".
    iDestruct (own_valid with "y") as "%val".
     iMod (own_sep_auth_incll_nondet γ (Inved p1) (Inved state)
@@ -475,27 +609,25 @@ Section StorageLogic.
     end)
      with "[x y]") as "x".
     {
-      intro. intro equi.
+      intro z. intro equi.
       assert (✓ Inved state) as val2. { generalize val. rewrite auth_auth_valid. trivial. }
-      have rr := own_sep_inv_incll_helper_nondet p1 state output_ok cond z pi val2 equi.
+      have rr := own_sep_inv_incll_helper_nondet p1 state t1 output_ok cond z pi val2 equi.
       destruct rr as [p2 [rr v]]. exists (Inved p2). split; trivial.
     }
     { iFrame. }
     iDestruct "x" as (z p2) "[%eq [frag auth]]".
     destruct eq as [big_oo eq].
-    destruct p2. { intuition. }
-    rename p into p2.
-    destruct z.
+    destruct p2 as [|p2]. { intuition. }
+    destruct z as [|p].
     {
       have eq0 := op_nah _ _ eq.
       assert (Inved p2 ⋅ Nah ≡ Inved p2) as eq1 by trivial.
       setoid_rewrite eq1.
       iExists (ε:P).
       assert (p2 ⋅ ε ≡ p2) as eq2.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
+      { 
+        rewrite (ra_comm _ (protocol_ra_mixin _ _ storage_mixin)).
+        apply (protocol_unit_left_id _ _ storage_mixin).
       }
       iModIntro. iExists p2.
       setoid_rewrite eq2.
@@ -503,10 +635,9 @@ Section StorageLogic.
       iPureIntro.
       split. { trivial. }
       assert (p1 ⋅ ε ≡ p1) as eq3.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
+      { 
+        rewrite (ra_comm _ (protocol_ra_mixin _ _ storage_mixin)).
+        apply (protocol_unit_left_id _ _ storage_mixin).
       }
       setoid_rewrite eq3. symmetry. trivial.
     }
@@ -518,16 +649,16 @@ Section StorageLogic.
       iModIntro. iExists p2. iFrame.
       iPureIntro. split. { apply big_oo. } symmetry. apply op_inved_inved. trivial.
     }
-   Qed.
+  Qed.
    
   Lemma own_inved_op_both (a b: P) γ :
       own γ (◯ Inved a) ∗ own γ (◯ Inved b) ⊣⊢ own γ (◯ Inved (a ⋅ b)).
   Proof.
     rewrite <- own_op.
     replace (◯ Inved a ⋅ ◯ Inved b) with (@auth_frag
-          (@inved_protocolUR P H4 H5 H6 H7 H8 H9 equ
-             (@protocol_mixin P B H4 H5 H6 H8 H7 H9 equ H H0 H1 H2 H3 H10 storage_mixin))
-          (@Inved P (@op P H6 a b))); trivial.
+          (inved_protocolUR
+                          (internal_protocol_mixin_storage_mixin storage_mixin))
+          (@Inved P (a ⋅ b))); trivial.
   Qed.
           
   Lemma own_inved_op (a b: P) γ :
@@ -538,125 +669,47 @@ Section StorageLogic.
       own γ (◯ Inved (a ⋅ b)) ⊢ own γ (◯ Inved a) ∗ own γ (◯ Inved b).
   Proof. rewrite own_inved_op_both. trivial. Qed.
     
-  (*
-  Lemma logic_exchange
-    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ)
-    (exchng: storage_protocol_exchange p1 p2 b1 b2)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[%wfm [#ounit #m]] [p f]".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
-    { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state) "lat".
-    iDestruct "lat" as "[ois [ps fi]]".
-    iMod "ois" as "ois".
-    iMod "ps" as "%ps".
-    unfold p_own.
-    iMod (own_sep_inv_incll γ p1 p2 state with "[p ois]") as (z) "[%incll [p ois]]".
-    { unfold storage_protocol_exchange in exchng. intros q pi.
-        have exch := exchng q pi. intuition. }
-    { iFrame. }
-    
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state)
-          ≡ f(interp (p1 ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    have exch := exchng z pinv_p1_z.
-    destruct exch as [pinv_p2_z [val_interp1 interp_eq]].
-    assert (✓ (interp (p2 ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[ois fi]"
-          as "inv_to_return".
-    {
-      iModIntro. (* strip later *)
-      iExists (p2 ⋅ z). iFrame "ois". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
-    { iFrame "m". iFrame "inv_to_return". iFrame "w". iFrame "od". }
-    iModIntro. iModIntro. iFrame.
-  Qed.
-  *)
-   
-  Lemma logic_exchange_nondeterministic
-    (p1: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ)
+  Lemma sp_exchange_nondeterministic
+    (p1: P) (b1: B) (output_ok: P → B → Prop) (γ: gname) (f: B → iProp Σ)
     (exchng: storage_protocol_exchange_nondeterministic p1 b1 output_ok)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗
-          ∃ p2 b2 , ⌜ output_ok p2 b2 ⌝ ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
+    : sp_sto γ f ⊢
+        sp_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗
+          ∃ p2 b2 , ⌜ output_ok p2 b2 ⌝ ∗ sp_own γ p2 ∗ ▷ f b2.
+  Proof.
+    unfold sp_sto. rewrite sp_own_eq. unfold sp_own_def.
     iIntros "[%wfm [#ounit #m]] [p f]".
     rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
     iIntros "[w oe]".
     iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
     { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state) "lat".
+    iMod (bi.later_exist_except_0 with "latp") as (state_t) "lat".
     iDestruct "lat" as "[ois [ps fi]]".
     iMod "ois" as "ois".
     iMod "ps" as "%ps".
-    unfold p_own.
-    iMod (own_sep_inv_incll_nondet γ p1 state (λ p2 q , ∃ b2 , output_ok p2 b2
-          /\ pinv (p2 ⋅ q)
-          /\ ✓(interp (p1 ⋅ q) ⋅ b1)
-          /\ interp (p1 ⋅ q) ⋅ b1 ≡ interp (p2 ⋅ q) ⋅ b2) with "[p ois]")
+    unfold sp_own.
+    iMod (own_sep_inv_incll_nondet γ p1 state_t.1 state_t.2 (λ p2 q , ∃ b2 t2 , output_ok p2 b2
+          ∧ sp_rel (p2 ⋅ q) t2
+          ∧ ✓(state_t.2 ⋅ b1)
+          ∧ state_t.2 ⋅ b1 ≡ t2 ⋅ b2) with "[p ois]")
         as (z p2) "[[%big_output_ok %incll] [p ois]]".
     { unfold storage_protocol_exchange in exchng. intros q pi.
-        have exch := exchng q pi. destruct exch as [p2 [b2 exch]]. exists p2. intuition. exists b2. intuition. }
+        have exch := exchng q state_t.2 pi. destruct exch as [p2 [b2 [t2 exch]]]. exists p2. exists t2. intuition. exists b2. exists t2. intuition. }
     { trivial. }
     { iFrame. }
-    destruct big_output_ok as [b2 [oo [pix [vix interp_eq]]]].
+    destruct big_output_ok as [b2 [t2 [oo [pix [vix interp_eq]]]]].
     
     destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
     
-    assert (f (interp state)
-          ≡ f(interp (p1 ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    setoid_rewrite equiv_interp_state.
     iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
     
     unfold storage_protocol_exchange in exchng.
     assert (pinv (p1 ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
+        exists (state_t.2). setoid_rewrite <- incll. trivial.
     }
 
-    assert (✓ (interp (p2 ⋅ z) ⋅ b2)) as val_interp2.
+    assert (✓ (t2 ⋅ b2)) as val_interp2.
     {
-      destruct storage_mixin. destruct base_ra_mixin0.
+      destruct (base_ra_mixin _ _ storage_mixin).
       setoid_rewrite <- interp_eq. trivial.
     }
     
@@ -667,13 +720,13 @@ Section StorageLogic.
     
     iDestruct "f_op" as "[fi fb]".
 
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
+    iAssert ((▷ ∃ (state0_t0 : P * B),
+          own γ (● Inved state0_t0.1) ∗ ⌜sp_rel state0_t0.1 state0_t0.2⌝ ∗ f state0_t0.2)%I)
           with "[ois fi]"
           as "inv_to_return".
     {
       iModIntro. (* strip later *)
-      iExists (p2 ⋅ z). iFrame "ois". iFrame "fi".
+      iExists (p2 ⋅ z, t2). iFrame "ois". iFrame "fi".
       iPureIntro. trivial.
     }
     iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
@@ -684,410 +737,32 @@ Section StorageLogic.
    
   (* SP-Exchange *)
    
-  Lemma logic_exchange
-    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ)
+  Lemma sp_exchange
+    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B → iProp Σ)
     (exchng: storage_protocol_exchange p1 p2 b1 b2)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+    : sp_sto γ f ⊢
+        sp_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ sp_own γ p2 ∗ ▷ f b2.
+  Proof.
     iIntros "x y".
-    iDestruct (logic_exchange_nondeterministic p1 b1 (λ p b, p = p2 ∧ b = b2) γ f with "x y") as "J".
+    iDestruct (sp_exchange_nondeterministic p1 b1 (λ p b, p = p2 ∧ b = b2) γ f with "x y") as "J".
     { unfold storage_protocol_exchange in exchng.
       unfold storage_protocol_exchange_nondeterministic.
-      intros q pi. exists p2. exists b2.
-      have ex := exchng q pi. intuition.
+      intros q t1 pi. exists p2. exists b2.
+      have ex := exchng q t1 pi. destruct ex as [t2 ex]. exists t2. intuition.
     }
     iMod "J" as (p0 b0) "[[%eq1 %eq2] t]". iModIntro. rewrite eq1. rewrite eq2. iFrame.
   Qed.
    
-   (*
-  Lemma logic_exchange_with_extra_guard
-    (p1 p2 q: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ)
-    (exchng: storage_protocol_exchange (p1 ⋅ q) (p2 ⋅ q) b1 b2)
-    : maps γ f ∗ □ (G &&{ {[ γ ]} }&&$> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[[%wfm [#ounit #m]] [#gu #kbi]] [g [p f]]".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
-    { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state) "lat".
-    unfold fguards, guards_with.
-    iDestruct ("gu" $! G) as "gu2".
-    
-    iDestruct ("gu2" with "[g lat]") as "gu3".
-    { iFrame "g". iIntros "g". iFrame "g".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iExists ((∃ state0 : P, own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I).
-        iFrame "m".
-        setoid_rewrite know_bulk_inv_singleton. unfold know_inv.
-        iModIntro. iExists state. iFrame "lat".
-    }
-    
-    iMod "gu3" as "[po b]".
-    
-     iAssert ((own γ (◯ Inved q) ∧
-          (◇ ∃ state : P, G ∗ ▷
-                (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state))))%I)
-          with "[po b]" as "x".
-      { iSplit. { iFrame. } 
-        iDestruct ("b" with "po") as "[ex t]".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iDestruct "ex" as (P0) "[#own lat]".
-        iDestruct (ownIagree γ P0 _ with "[m own]") as "eq".
-        { iSplitL. { iFrame "own". } iFrame "m". }
-        iRewrite "eq" in "lat".
-        iMod (bi.later_exist_except_0 with "lat") as (state0) "lat".
-        iExists state0. iFrame.
-      }
-      iMod (and_except0_r with "x") as "x".
-      rewrite bi.and_exist_l.
-      iDestruct "x" as (state0) "x".
-      iMod (apply_timeless with "x") as "x".
-      iDestruct (stuff1 with "x") as "%pinvs".
-      unfold p_own.
-      (*iDestruct (stuff3 γ p1 q state0 with "[p x]") as "%incll". { iFrame. }*)
-      
-      iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0) ∗ (G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)))%I with "[x]" as "x".
-      { iSplit. { iDestruct "x" as "[x _]". iFrame. }
-          iDestruct "x" as "[_ [x [y z]]]". iFrame. }
-      iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
-      { apply auth_frag_disjointness. }
-      iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)) with "[y]") as "[y z]".
-      { iFrame "y". iIntros "[k _]". iFrame. }
-      
-      iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-      iMod (own_sep_inv_incll γ (p1 ⋅ q) (p2 ⋅ q) state0 with "[own_p_q x]")
-          as (z) "[%incll [own_p_q x]]".
-      { unfold storage_protocol_exchange in exchng.
-        intro q0. have exq := exchng q0. intuition. }
-      { iFrame. }
-      
-      iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-      iDestruct ("z" with "q") as "[_ z]".
-       
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    iDestruct "z" as "[g [_ fi]]".
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    have exch := exchng z pinv_p1_z.
-    destruct exch as [pinv_p2_z [val_interp1 interp_eq]].
-    assert (✓ (interp (p2 ⋅ q ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[x fi]"
-          as "inv_to_return".
-    {
-      iModIntro. (* strip later *)
-      iExists (p2 ⋅ q ⋅ z). iFrame "x". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
-    { iFrame "m". iFrame "inv_to_return". iFrame "w". iFrame "od". }
-    iModIntro. iModIntro. iFrame.
-  Qed.
-  *)
-  
-  (*
-  Lemma logic_exchange_with_extra_guard_nondeterministic
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ)
-    (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
-    : maps γ f ∗ □ (G &&{ {[ γ ]} }&&$> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[[%wfm [#ounit #m]] [#gu #kbi]] [g [p f]]".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
-    { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state) "lat".
-    unfold fguards, guards_with.
-    iDestruct ("gu" $! G) as "gu2".
-    
-    iDestruct ("gu2" with "[g lat]") as "gu3".
-    { iFrame "g". iIntros "g". iFrame "g".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iExists ((∃ state0 : P, own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I).
-        iFrame "m".
-        setoid_rewrite know_bulk_inv_singleton. unfold know_inv.
-        iModIntro. iExists state. iFrame "lat".
-    }
-    
-    iMod "gu3" as "[po b]".
-    
-     iAssert ((own γ (◯ Inved q) ∧
-          (◇ ∃ state : P, G ∗ ▷
-                (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state))))%I)
-          with "[po b]" as "x".
-      { iSplit. { iFrame. } 
-        iDestruct ("b" with "po") as "[ex t]".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iDestruct "ex" as (P0) "[#own lat]".
-        iDestruct (ownIagree γ P0 _ with "[m own]") as "eq".
-        { iSplitL. { iFrame "own". } iFrame "m". }
-        iRewrite "eq" in "lat".
-        iMod (bi.later_exist_except_0 with "lat") as (state0) "lat".
-        iExists state0. iFrame.
-      }
-      iMod (and_except0_r with "x") as "x".
-      rewrite bi.and_exist_l.
-      iDestruct "x" as (state0) "x".
-      iMod (apply_timeless with "x") as "x".
-      iDestruct (stuff1 with "x") as "%pinvs".
-      unfold p_own.
-      (*iDestruct (stuff3 γ p1 q state0 with "[p x]") as "%incll". { iFrame. }*)
-      
-      iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0) ∗ (G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)))%I with "[x]" as "x".
-      { iSplit. { iDestruct "x" as "[x _]". iFrame. }
-          iDestruct "x" as "[_ [x [y z]]]". iFrame. }
-      iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
-      { apply auth_frag_disjointness. }
-      iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)) with "[y]") as "[y z]".
-      { iFrame "y". iIntros "[k _]". iFrame. }
-      
-      iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-      iMod (own_sep_inv_incll_nondet γ (p1 ⋅ q) state0 (λ p2_q r , ∃ p2 b2 , p2_q = p2 ⋅ q /\ output_ok p2 b2
-          /\ pinv ((p2 ⋅ q) ⋅ r)
-          /\ ✓(interp ((p1 ⋅ q) ⋅ r) ⋅ b1)
-          /\ interp ((p1 ⋅ q) ⋅ r) ⋅ b1 ≡ interp ((p2 ⋅ q) ⋅ r) ⋅ b2) with "[own_p_q x]")
-          as (z p2_q) "[%incll [own_p_q x]]".
-      { unfold storage_protocol_exchange_nondeterministic in exchng.
-        intro r. intro j0. have exq := exchng r j0.
-        destruct exq as [p2_q [b2 exq]].
-        destruct exq as [[p2 [eq oo]] [a b]].
-        exists (p2 ⋅ q). split.
-        { exists p2. exists b2. intuition. { rewrite <- eq. apply a. }
-            rewrite <- eq. trivial. }
-        { rewrite <- eq. apply a. }
-      }
-      { apply pinvs. }
-      { iFrame. }
-      
-      destruct incll as [[p2 [b2 [p2_q_eq bigconj]]] incll].
-      rewrite p2_q_eq.
-      iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-      iDestruct ("z" with "q") as "[_ z]".
-      
-      destruct bigconj as [oo [pix [iix interp_eq]]].
-       
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    iDestruct "z" as "[g [_ fi]]".
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    assert (✓ (interp (p2 ⋅ q ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[x fi]"
-          as "inv_to_return".
-    {
-      iModIntro. (* strip later *)
-      iExists (p2 ⋅ q ⋅ z). iFrame "x". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
-    { iFrame "m". iFrame "inv_to_return". iFrame "w". iFrame "od". }
-    iModIntro. iModIntro. iFrame. iExists p2. iExists b2. iFrame. iPureIntro. trivial.
-  Qed.
-  *)
-  
-  (*
-  Lemma logic_exchange_with_extra_guard_nondeterministic2
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ) E
-    (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
-    (gname_in_e: γ ∈ E)
-    : maps γ f ∗ □ (G &&{ E }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ E }=∗ ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[[%wfm [#ounit #m]] #gu] [g [p f]]".
-    iDestruct (guards_from_inv _ _ E with "m") as "mg". { set_solver. }
-    iDestruct (guards_true E G) as "gt".
-    iDestruct (guards_transitive _ G True%I with "[gt mg]") as "gg".
-    { iFrame "gt". iFrame "mg". }
-    iDestruct (guards_open_two_simultaneously G _ _ E E with "[g gg gu]") as "opened".
-    { set_solver. }
-    { iFrame "g". iSplit. { iFrame "gg". } iFrame "gu". }
-    iMod "opened" as (T) "[t [tinv [town back]]]".
-    
-    iAssert ((◇ own γ (◯ Inved q) ∧ (
-          ◇ (▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T)
-          ∗
-          ◇ (∃ state : P, ▷
-                (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)))
-          ))%I)
-          with "[t tinv town]" as "x".
-    { iSplit. { iMod ("town" with "t") as "town". unfold p_own.
-        iDestruct "town" as "[x y]". iModIntro. iFrame "x". }
-        iDestruct ("tinv" with "t") as "[tinv back]".
-        iFrame "back".
-        iMod "tinv" as "tinv".
-        iMod (bi.later_exist_except_0 with "tinv") as (state0) "tinv".
-        iModIntro.
-        iExists state0.
-        iFrame "tinv".
-    }
-    
-    rewrite <- bi.except_0_sep.
-    rewrite <- bi.except_0_and.
-    iMod "x" as "x".
-    
-    rewrite bi.sep_exist_l.
-    rewrite bi.and_exist_l.
-    iDestruct "x" as (state0) "x".
-    iMod (apply_timeless with "x") as "x".
-    iDestruct (stuff1 with "x") as "%pinvs".
-    unfold p_own.
-    
-    iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0) ∗ ((▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T) ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)))%I with "[x]" as "x".
-      { iSplit. { iDestruct "x" as "[x _]". iFrame. }
-          iDestruct "x" as "[_ [x [y z]]]". iFrame. }
-          
-    iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
-      { apply auth_frag_disjointness. }
-      
-    iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ (▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T) ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)) with "[y]") as "[y z]".
-      { iFrame "y". iIntros "[k _]". iFrame. }
-      
-    iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-    iMod (own_sep_inv_incll_nondet γ (p1 ⋅ q) state0 (λ p2_q r , ∃ p2 b2 , p2_q = p2 ⋅ q /\ output_ok p2 b2
-          /\ pinv ((p2 ⋅ q) ⋅ r)
-          /\ ✓(interp ((p1 ⋅ q) ⋅ r) ⋅ b1)
-          /\ interp ((p1 ⋅ q) ⋅ r) ⋅ b1 ≡ interp ((p2 ⋅ q) ⋅ r) ⋅ b2) with "[own_p_q x]")
-          as (z p2_q) "[%incll [own_p_q x]]".
-      { unfold storage_protocol_exchange_nondeterministic in exchng.
-        intro r. intro j0. have exq := exchng r j0.
-        destruct exq as [p2_q [b2 exq]].
-        destruct exq as [[p2 [eq oo]] [a b]].
-        exists (p2 ⋅ q). split.
-        { exists p2. exists b2. intuition. { rewrite <- eq. apply a. }
-            rewrite <- eq. trivial. }
-        { rewrite <- eq. apply a. }
-      }
-      { apply pinvs. }
-      { iFrame. }
-      
-      destruct incll as [[p2 [b2 [p2_q_eq bigconj]]] incll].
-      rewrite p2_q_eq.
-      iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-      iDestruct ("z" with "q") as "[_ z]".
-      
-      destruct bigconj as [oo [pix [iix interp_eq]]].
-       
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    iDestruct "z" as "[g [_ fi]]".
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    assert (✓ (interp (p2 ⋅ q ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[x fi]"
-          as "inv_to_return".
-    {
-      iModIntro.
-      iExists (p2 ⋅ q ⋅ z). iFrame "x". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct ("g" with "inv_to_return") as "g".
-    iMod ("back" with "g") as "g".
-    iModIntro. iFrame. iExists p2. iExists b2. iFrame. iPureIntro. trivial.
-  Qed.
-  *)
-    
-  Lemma logic_exchange_with_extra_guard_nondeterministic_with_later
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ) E n
+  Lemma sp_exchange_with_extra_guard_nondeterministic_with_later
+    (p1 q: P) (b1: B) (output_ok: P → B → Prop) (γ: gname) (f: B → iProp Σ) (G: iProp Σ) E n
     (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
+        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q ∧ output_ok p2 b2))
     (gname_in_e: γ ∈ E)
-    : maps γ f ∗ (G &&{ E ; n }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ E, ∅ }=∗ ▷^n (|={ ∅, E }=> ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
+    : sp_sto γ f ∗ (G &&{ E ; n }&&> sp_own γ q) ⊢
+        G ∗ sp_own γ p1 ∗ ▷ f b1 ={ E, ∅ }=∗ ▷^n (|={ ∅, E }=> ∃ p2 b2 ,
+            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ sp_own γ p2 ∗ ▷ f b2).
+  Proof.
+    unfold sp_sto. rewrite sp_own_eq. unfold sp_own_def.
     iIntros "[[%wfm [#ounit #m]] #gu] [g [p f]]".
     iDestruct (guards_from_inv _ _ E with "m") as "mg". { set_solver. }
     iDestruct (guards_true E G) as "gt".
@@ -1101,13 +776,13 @@ Section StorageLogic.
     iMod "opened" as (T) "[t [tinv [town back]]]".
     
     iAssert ((▷^n (◇ own γ (◯ Inved q) ∧ (
-          ◇ (▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T)
+          ◇ (▷ (∃ state_t : (P * B), own γ (● Inved state_t.1) ∗ ⌜sp_rel state_t.1 state_t.2⌝ ∗ f state_t.2) -∗ T)
           ∗
-          ◇ (∃ state : P, ▷
-                (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)))
+          ◇ (∃ state_t : (P * B), ▷
+                (own γ (● Inved state_t.1) ∗ ⌜sp_rel state_t.1 state_t.2⌝ ∗ f state_t.2))
           )))%I)
           with "[t tinv town]" as "x".
-    { iSplit. { iDestruct ("town" with "t") as "town". iNext. unfold p_own.
+    { iSplit. { iDestruct ("town" with "t") as "town". iNext. unfold sp_own.
         iDestruct "town" as "[x y]". iFrame "x". }
         iDestruct ("tinv" with "t") as "[tinv back]".
         iFrame "back". iNext. iMod "tinv" as "tinv".
@@ -1125,66 +800,58 @@ Section StorageLogic.
     rewrite bi.sep_exist_l.
     rewrite bi.and_exist_l.
     iDestruct "x" as (state0) "x".
-    iMod (apply_timeless with "x") as "x".
-    iDestruct (stuff1 with "x") as "%pinvs".
-    unfold p_own.
+    iMod (apply_timeless_rhs4 with "x") as "x".
+    iDestruct (and_rhs3_entails with "x") as "%pinvs".
+    unfold sp_own.
     
-    iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0) ∗ ((▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T) ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)))%I with "[x]" as "x".
+    iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0.1) ∗ ((▷ (∃ state_t : P * B, own γ (● Inved state_t.1) ∗ ⌜sp_rel state_t.1 state_t.2⌝ ∗ f state_t.2) -∗ T) ∗ ⌜sp_rel state0.1 state0.2⌝ ∗ ▷ f state0.2))%I with "[x]" as "x".
       { iSplit. { iDestruct "x" as "[x _]". iFrame. }
           iDestruct "x" as "[_ [x [y z]]]". iFrame. }
           
     iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
       { apply auth_frag_disjointness. }
       
-    iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ (▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T) ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)) with "[y]") as "[y z]".
+    iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ (▷ (∃ state_t : P * B, own γ (● Inved state_t.1) ∗ ⌜sp_rel state_t.1 state_t.2⌝ ∗ f state_t.2) -∗ T) ∗ ⌜sp_rel state0.1 state0.2⌝ ∗ ▷ f state0.2) with "[y]") as "[y z]".
       { iFrame "y". iIntros "[k _]". iFrame. }
       
     iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-    iMod (own_sep_inv_incll_nondet γ (p1 ⋅ q) state0 (λ p2_q r , ∃ p2 b2 , p2_q = p2 ⋅ q /\ output_ok p2 b2
-          /\ pinv ((p2 ⋅ q) ⋅ r)
-          /\ ✓(interp ((p1 ⋅ q) ⋅ r) ⋅ b1)
-          /\ interp ((p1 ⋅ q) ⋅ r) ⋅ b1 ≡ interp ((p2 ⋅ q) ⋅ r) ⋅ b2) with "[own_p_q x]")
+    iMod (own_sep_inv_incll_nondet γ (p1 ⋅ q) state0.1 state0.2 (λ p2_q r , ∃ p2 b2 t2 , p2_q = p2 ⋅ q ∧ output_ok p2 b2
+          ∧ sp_rel ((p2 ⋅ q) ⋅ r) t2
+          ∧ ✓(state0.2 ⋅ b1)
+          ∧ state0.2 ⋅ b1 ≡ t2 ⋅ b2) with "[own_p_q x]")
           as (z p2_q) "[%incll [own_p_q x]]".
       { unfold storage_protocol_exchange_nondeterministic in exchng.
-        intro r. intro j0. have exq := exchng r j0.
-        destruct exq as [p2_q [b2 exq]].
+        intro r. intro j0. have exq := exchng r state0.2 j0.
+        destruct exq as [p2_q [b2 [t2 exq]]].
         destruct exq as [[p2 [eq oo]] [a b]].
-        exists (p2 ⋅ q). split.
-        { exists p2. exists b2. intuition. { rewrite <- eq. apply a. }
-            rewrite <- eq. trivial. }
+        exists (p2 ⋅ q). exists t2. split.
+        { exists p2. exists b2. exists t2. intuition. rewrite <- eq. apply a. }
         { rewrite <- eq. apply a. }
       }
-      { apply pinvs. }
-      { iFrame. }
-      
-      destruct incll as [[p2 [b2 [p2_q_eq bigconj]]] incll].
-      rewrite p2_q_eq.
-      iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-      iDestruct ("z" with "q") as "[_ z]".
+    { trivial. }
+    { iFrame. }
       
-      destruct bigconj as [oo [pix [iix interp_eq]]].
+    destruct incll as [[p2 [b2 [t2 [p2_q_eq bigconj]]]] incll].
+    rewrite p2_q_eq.
+    iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
+    iDestruct ("z" with "q") as "[_ z]".
+
+    destruct bigconj as [oo [pix [iix interp_eq]]].
        
     destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
     
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
     iDestruct "z" as "[g [_ fi]]".
-    setoid_rewrite equiv_interp_state.
     iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
     
     unfold storage_protocol_exchange in exchng.
     assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
+        setoid_rewrite <- incll. exists (state0.2).
+        apply pinvs.
     }
 
-    assert (✓ (interp (p2 ⋅ q ⋅ z) ⋅ b2)) as val_interp2.
+    assert (✓ (t2 ⋅ b2)) as val_interp2.
     {
-      destruct storage_mixin. destruct base_ra_mixin0.
+      destruct (base_ra_mixin _ _ storage_mixin).
       setoid_rewrite <- interp_eq. trivial.
     }
     
@@ -1195,13 +862,13 @@ Section StorageLogic.
     
     iDestruct "f_op" as "[fi fb]".
 
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
+    iAssert ((▷ ∃ state0_t : P * B,
+          own γ (● Inved state0_t.1) ∗ ⌜sp_rel state0_t.1 state0_t.2⌝ ∗ f state0_t.2)%I)
           with "[x fi]"
           as "inv_to_return".
     {
       iModIntro.
-      iExists (p2 ⋅ q ⋅ z). iFrame "x". iFrame "fi".
+      iExists (p2 ⋅ q ⋅ z, t2). iFrame "x". iFrame "fi".
       iPureIntro. trivial.
     }
     iDestruct ("g" with "inv_to_return") as "g".
@@ -1209,31 +876,32 @@ Section StorageLogic.
     iModIntro. iFrame. iPureIntro. trivial.
   Qed.
   
-  Lemma logic_exchange_with_extra_guard_nondeterministic
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ) E
+  Lemma sp_exchange_with_extra_guard_nondeterministic
+    (p1 q: P) (b1: B) (output_ok: P → B → Prop) (γ: gname) (f: B → iProp Σ) (G: iProp Σ) E
     (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
+        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q ∧ output_ok p2 b2))
     (gname_in_e: γ ∈ E)
-    : maps γ f ∗ (G &&{ E }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ E }=∗ ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+    : sp_sto γ f ∗ (G &&{ E }&&> sp_own γ q) ⊢
+        G ∗ sp_own γ p1 ∗ ▷ f b1 ={ E }=∗ ∃ p2 b2 ,
+            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ sp_own γ p2 ∗ ▷ f b2.
+  Proof.
     iIntros "x y".
-    iDestruct (logic_exchange_with_extra_guard_nondeterministic_with_later p1 q b1 output_ok γ f G E 0 exchng gname_in_e with "x y") as "J".
+    iDestruct (sp_exchange_with_extra_guard_nondeterministic_with_later p1 q b1 output_ok γ f G E 0 exchng gname_in_e with "x y") as "J".
     iMod "J". iMod "J". iModIntro. iFrame.
   Qed.
   
-  Lemma logic_exchange_with_extra_guard
-    (p1 p2 q: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ)
+  Lemma sp_exchange_with_extra_guard
+    (p1 p2 q: P) (b1 b2: B) (γ: gname) (f: B → iProp Σ) (G: iProp Σ)
     (exchng: storage_protocol_exchange (p1 ⋅ q) (p2 ⋅ q) b1 b2)
-    : maps γ f ∗ (G &&{ {[ γ ]} }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+    : sp_sto γ f ∗ (G &&{ {[ γ ]} }&&> sp_own γ q) ⊢
+        G ∗ sp_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ G ∗ sp_own γ p2 ∗ ▷ f b2.
+  Proof.
     iIntros "x y".
-    iDestruct (logic_exchange_with_extra_guard_nondeterministic p1 q b1 (λ p b, p = p2 ∧ b = b2) γ f G {[ γ ]} with "x y") as "J".
+    iDestruct (sp_exchange_with_extra_guard_nondeterministic p1 q b1 (λ p b, p = p2 ∧ b = b2) γ f G {[ γ ]} with "x y") as "J".
     { unfold storage_protocol_exchange_nondeterministic.
       unfold storage_protocol_exchange in exchng.
-      intros q0 pi. exists (p2 ⋅ q). exists b2. have ex := exchng q0 pi.
+      intros q0 t1 pi. exists (p2 ⋅ q). exists b2. have ex := exchng q0 t1 pi.
+      destruct ex as [t2 ex]. exists t2.
       split. { exists p2. split; trivial. split; trivial. }
       apply ex.
     }
@@ -1241,91 +909,43 @@ Section StorageLogic.
     iMod "J" as (p0 b0) "[[%es %es2] L]". iModIntro. subst p0. subst b0. iFrame.
   Qed.
   
-  (*
-  Lemma logic_exchange_nondeterministic
-    (p1: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ)
-    (exchng: storage_protocol_exchange_nondeterministic p1 b1 output_ok)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗
-          ∃ p2 b2 , ⌜ output_ok p2 b2 ⌝ ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "maps p_own".
-    iDestruct (logic_exchange_with_extra_guard_nondeterministic p1 ε b1 output_ok γ f True {[ γ ]}) as "J".
-    { unfold storage_protocol_exchange_nondeterministic in *. intros q pi.
-      assert (p1 ⋅ ε ≡ p1) as X. {
-        destruct storage_mixin. destruct protocol_mixin.
-        rewrite ra_comm; trivial.
-      }
-      assert (pinv (p1 ⋅ q)) as Y. {
-        destruct storage_mixin. destruct protocol_mixin.
-          apply inv_proper with (x := (p1 ⋅ ε) ⋅ q); trivial.
-          rewrite ra_comm; trivial.
-          setoid_replace (p1 ⋅ q) with (q ⋅ p1) by (rewrite ra_comm; trivial).
-          have op_proper := (ra_op_proper P protocol_ra_mixin).
-          unfold Proper, "==>", impl in op_proper.
-          have opp := op_proper q (p1 ⋅ ε) p1.
-          apply opp. apply X.
-      }
-      
-      have ex := exchng q Y.
-      destruct ex as [p2 [b2 [oo [pi2 in2]]]].
-      exists (p2 ⋅ ε). exists b2.
-      
-      assert (p2 ⋅ ε ≡ p2) as Z. {
-        destruct storage_mixin. destruct protocol_mixin.
-        rewrite ra_comm; trivial.
-      }
-      assert (pinv (p2 ⋅ ε ⋅ q)) as W. {
-        destruct storage_mixin. destruct protocol_mixin.
-          apply inv_proper with (x := (p2 ⋅ q)); trivial.
-          rewrite ra_comm; trivial.
-          setoid_replace (p2 ⋅ ε ⋅ q) with (q ⋅ (p2 ⋅ ε)) by (rewrite ra_comm; trivial).
-          have op_proper := (ra_op_proper P protocol_ra_mixin).
-          unfold Proper, "==>", impl in op_proper.
-          have opp := op_proper q p2 (p2 ⋅ ε).
-          apply opp. symmetry. apply Z.
-      }
-      intuition.
-      { exists p2. split; trivial. }
-   *)   
-
-    
-  
-  Lemma inved_op (a b : P) :
+  Local Lemma inved_op (a b : P) :
       Inved (a ⋅ b) ≡ Inved a ⋅ Inved b.
-  Proof using H4 H6 H7 P equ. trivial. Qed.
+  Proof using equ_p. trivial. Qed.
 
   (* SP-Sep *)
 
-  Lemma p_own_op a b γ :
-      p_own γ (a ⋅ b) ⊣⊢ p_own γ a ∗ p_own γ b.
+  Lemma sp_own_op a b γ :
+      sp_own γ (a ⋅ b) ⊣⊢ sp_own γ a ∗ sp_own γ b.
   Proof.
-    unfold p_own.
+    rewrite sp_own_eq. unfold sp_own_def.
     setoid_rewrite inved_op.
     rewrite auth_frag_op.
     apply own_op.
   Qed.
   
+  (* TODO
+  Lemma sp_own_and x y γ :
+      sp_own γ x ∧ sp_own γ y ⊢ ∃ z , ⌜ x ≼ z ∧ y ≼ z ⌝ ∗ sp_own γ z.
+  Proof.
+    iIntros "H". unfold sp_own. iDestruct (and_own_discrete_ucmra with "H") as (z) "[J %t]".
+    destruct t as [Hxz Hyz]. destruct z as [|p].
+  Qed.
+  *)
+  
   Lemma op_unit (p: P) : p ⋅ ε ≡ p.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct protocol_mixin.
-    destruct protocol_ra_mixin.
-    setoid_rewrite (@comm P).
-    - apply protocol_unit_left_id.
-    - trivial.
+  Proof using storage_mixin.
+    rewrite (ra_comm _ (protocol_ra_mixin _ _ storage_mixin)).
+    apply (protocol_unit_left_id _ _ storage_mixin).
   Qed.
   
   Lemma op_unit_base (b: B) : b ⋅ ε ≡ b.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct base_ra_mixin0.
-    setoid_rewrite (@comm B).
-    - apply base_unit_left_id0.
-    - trivial.
+  Proof using storage_mixin.
+    rewrite (ra_comm _ (base_ra_mixin _ _ storage_mixin)).
+    apply (base_unit_left_id _ _ storage_mixin).
   Qed.
   
-  Lemma auth_inved_conjure_unit γ (state: P)
+  Local Lemma auth_inved_conjure_unit γ (state: P)
       : own γ (● Inved state) ==∗ own γ (● Inved state) ∗ own γ (◯ Inved ε).
   Proof.
       apply auth_conjure_frag.
@@ -1333,28 +953,34 @@ Section StorageLogic.
       setoid_rewrite op_unit.
       trivial.
   Qed.
+   
+  Local Lemma valid_inved_of_pinv (p: P)
+    : pinv p → ✓ (Inved p). 
+  Proof using storage_mixin.
+    intro pi. unfold "✓", inved_protocol_valid. exists ε. setoid_rewrite op_unit.
+    trivial.
+  Qed.
 
   (* SP-Unit *)
   
-  Lemma p_own_unit γ f
-      : maps γ f ⊢ p_own γ ε.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
+  Lemma sp_own_unit γ f
+      : sp_sto γ f ⊢ sp_own γ ε.
+  Proof.
+    unfold sp_sto. rewrite sp_own_eq. unfold sp_own_def.
     iIntros "[%wfm [#ounit #m]]".
-    unfold p_own.
     iFrame "ounit".
   Qed.
 
   (* SP-Deposit *)
     
-  Lemma logic_deposit
-      (p1 p2: P) (b1: B) (γ: gname) (f: B -> iProp Σ)
+  Lemma sp_deposit
+      (p1 p2: P) (b1: B) (γ: gname) (f: B → iProp Σ)
       (exchng: storage_protocol_deposit p1 p2 b1)
-      : maps γ f ⊢
-          p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ p_own γ p2.
-   Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+      : sp_sto γ f ⊢
+          sp_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ sp_own γ p2.
+  Proof.
     iIntros "#m pb".
-    iMod (logic_exchange p1 p2 b1 (ε: B) γ f with "m pb") as "[pb u]".
+    iMod (sp_exchange p1 p2 b1 (ε: B) γ f with "m pb") as "[pb u]".
     {
       unfold storage_protocol_exchange.
       unfold storage_protocol_deposit in exchng.
@@ -1363,107 +989,87 @@ Section StorageLogic.
       trivial.
     }
     iModIntro. iFrame "pb".
-   Qed.
+  Qed.
    
   Instance valid_proper_base : Proper ((≡) ==> impl) (@valid B _).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct base_ra_mixin0.
-    apply ra_validN_proper.
+  Proof using storage_mixin.
+    apply (ra_validN_proper _ (base_ra_mixin _ _ storage_mixin)).
   Qed.
   
-  Instance pinv_proper : Proper ((≡) ==> impl) (@pinv P _).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct protocol_mixin0.
-    apply inv_proper.
-  Qed.
-  
-  Lemma valid_interp (p: P)
-      : pinv p -> ✓ (interp p).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    apply interp_val0.
-  Qed.
-
   (* SP-Withdraw *)
    
-  Lemma logic_withdraw
-      (p1 p2: P) (b2: B) (γ: gname) (f: B -> iProp Σ)
+  Lemma sp_withdraw
+      (p1 p2: P) (b2: B) (γ: gname) (f: B → iProp Σ)
       (exchng: storage_protocol_withdraw p1 p2 b2)
-      : maps γ f ⊢
-          p_own γ p1 ={ {[ γ ]} }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+      : sp_sto γ f ⊢
+          sp_own γ p1 ={ {[ γ ]} }=∗ sp_own γ p2 ∗ ▷ f b2.
+  Proof.
     iIntros "#m pb".
     iAssert (▷ f ε)%I as "u".
     {
       iModIntro. 
-      unfold maps.
+      unfold sp_sto.
       iDestruct "m" as "[%wf #m]".
       unfold wf_prop_map in wf.
       destruct wf as [wf_prop [wf_unit _]].
       setoid_rewrite wf_unit. done.
     }
-    iMod (logic_exchange p1 p2 (ε: B) b2 γ f with "m [pb u]") as "[pb fb2]".
+    iMod (sp_exchange p1 p2 (ε: B) b2 γ f with "m [pb u]") as "[pb fb2]".
     {
       unfold storage_protocol_exchange.
       unfold storage_protocol_withdraw in exchng.
-      intros q pi1. have t := exchng q pi1. intuition.
+      intros q t1 pi1. have j := exchng q t1 pi1. destruct j as [t2 j].
+      exists t2. intuition.
       - setoid_rewrite op_unit_base.
-        apply valid_interp. trivial.
+        destruct storage_mixin. apply (interp_val _ _ storage_mixin (p1 ⋅ q)). trivial.
       - setoid_rewrite op_unit_base. trivial.
     }
     { iFrame "pb". iFrame "u". }
     iModIntro. iFrame.
-   Qed.
+  Qed.
 
   (* SP-Update *)
    
-  Lemma logic_update
-      (p1 p2: P) (γ: gname) (f: B -> iProp Σ)
+  (* TODO It should be possible to do the update at mask ∅, but this requires changing
+     the underlying auth resource slightly. *)
+  Lemma sp_update
+      (p1 p2: P) (γ: gname) (f: B → iProp Σ)
       (exchng: storage_protocol_update p1 p2)
-      : maps γ f ⊢
-          p_own γ p1 ={ {[ γ ]} }=∗ p_own γ p2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+      : sp_sto γ f ⊢
+          sp_own γ p1 ={ {[ γ ]} }=∗ sp_own γ p2.
+  Proof.
     iIntros "#m pb".
-    iDestruct (logic_withdraw p1 p2 ε γ f with "m pb") as "pb".
+    iDestruct (sp_withdraw p1 p2 ε γ f with "m pb") as "pb".
     {
       unfold storage_protocol_withdraw.
       unfold storage_protocol_update in exchng.
-      intros q pi.
-      have exch := exchng q.
+      intros q t1 pi.
+      have exch := exchng q t1.
       intuition.
-      setoid_rewrite op_unit_base.
-      trivial.
+      setoid_rewrite op_unit_base. exists t1. split; trivial.
     }
     iMod "pb".
     iModIntro.
     iDestruct "pb" as "[pb _]".
     iFrame.
   Qed.
-  
-  Lemma valid_inved_of_pinv (p: P)
-    : pinv p -> ✓ (Inved p). 
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    intro pi. unfold "✓", inved_protocol_valid. exists ε. setoid_rewrite op_unit.
-    trivial.
-  Qed.
-
+ 
   (* SP-Alloc *)
   
-  Lemma logic_init_ns (p: P) (f: B -> iProp Σ) E (N: namespace)
-      (pi: pinv p) (wf: wf_prop_map f)
-  : ⊢ f (interp p) ={E}=∗ ∃ γ , ⌜ γ ∈ (↑ N : coPset) ⌝ ∗ maps γ f ∗ p_own γ p.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+  Lemma sp_alloc_ns (p: P) (b: B) (f: B → iProp Σ) E (N: namespace)
+      (pi: sp_rel p b) (wf: wf_prop_map f)
+  : ⊢ f b ={E}=∗ ∃ γ , ⌜ γ ∈ (↑ N : coPset) ⌝ ∗ sp_sto γ f ∗ sp_own γ p.
+  Proof.
     iIntros "f_init".
+    rewrite sp_own_eq. unfold sp_own_def.
     rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
     iIntros "[w oe]".
     iMod (ownI_alloc_and_simultaneous_own_alloc_ns
       (λ γ , 
-        (∃ (state: P) ,
-          own γ (● (Inved state))
-          ∗ ⌜ pinv state ⌝
-          ∗ (f (interp state)))%I
+        (∃ (state_t: P * B) ,
+          own γ (● (Inved state_t.1))
+          ∗ ⌜ sp_rel state_t.1 state_t.2 ⌝
+          ∗ (f state_t.2))%I
       )
       (● (Inved p) ⋅ (◯ (Inved ε) ⋅ ◯ (Inved p)))
       (↑ N)
@@ -1473,39 +1079,39 @@ Section StorageLogic.
       rewrite <- auth_frag_op.
       rewrite auth_both_valid_discrete. split; trivial.
       - replace (Inved ε ⋅ Inved p) with (Inved (ε ⋅ p)) by trivial.
-        destruct storage_mixin. destruct protocol_mixin0. rewrite protocol_unit_left_id.
+        rewrite (protocol_unit_left_id _ _ storage_mixin).
         trivial.
-      - apply valid_inved_of_pinv. trivial.
+      - apply valid_inved_of_pinv. exists b. apply pi.
     }
     
     iDestruct "w" as (γ) "[%in_ns [w [oinv [auth [u frag]]]]]".
     
     iDestruct ("w" with "[auth f_init]") as "w".
     {
-      iModIntro. iExists p. iFrame. iPureIntro. trivial.
+      iModIntro. iExists (p, b). iFrame. iPureIntro. trivial.
     }
     
     iModIntro. iModIntro.
     iFrame "w". iFrame "oe".
     iExists γ.
-    unfold p_own. iFrame "frag".
-    unfold maps.
+    unfold sp_own. iFrame "frag".
+    unfold sp_sto.
     iFrame "oinv". iFrame.
     iPureIntro. split; trivial.
   Qed.
   
-  Lemma logic_init (p: P) (f: B -> iProp Σ) E
-      (pi: pinv p) (wf: wf_prop_map f)
-  : ⊢ f (interp p) ={E}=∗ ∃ γ , maps γ f ∗ p_own γ p.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+  Lemma sp_alloc (p: P) (b: B) (f: B → iProp Σ) E
+      (pi: sp_rel p b) (wf: wf_prop_map f)
+  : ⊢ f b ={E}=∗ ∃ γ , sp_sto γ f ∗ sp_own γ p.
+  Proof.
     iIntros "f_init".
-    iMod (logic_init_ns p f E nroot with "f_init") as (γ) "[_ t]"; trivial.
+    iMod (sp_alloc_ns p b f E nroot with "f_init") as (γ) "[_ t]"; trivial.
     iModIntro. iExists γ. iFrame.
   Qed.
   
   Lemma fupd_singleton_mask_frame (γ: gname) (X Y Z : iProp Σ) E
     (premise: X ⊢ Y ={ {[ γ ]} }=∗ Z) (is_in: γ ∈ E) : X ⊢ Y ={ E }=∗ Z.
-  Proof using B H equb invGS0 Σ.
+  Proof.
     iIntros "x y".
     iDestruct (premise with "x y") as "p".
     iDestruct (fupd_mask_frame_r _ _ (E ∖ {[γ]}) with "p") as "p".
@@ -1518,66 +1124,94 @@ Section StorageLogic.
     trivial.
   Qed.
     
-  Lemma logic_exchange'
-    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ) E
+  Lemma sp_exchange'
+    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B → iProp Σ) E
     (exchng: storage_protocol_exchange p1 p2 b1 b2)
     (gname_in_e: γ ∈ E)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ E }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+    : sp_sto γ f ⊢
+        sp_own γ p1 ∗ ▷ f b1 ={ E }=∗ sp_own γ p2 ∗ ▷ f b2.
+  Proof.
     apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_exchange; trivial.
+    apply sp_exchange; trivial.
   Qed.
    
-  Lemma logic_deposit'
-      (p1 p2: P) (b1: B) (γ: gname) (f: B -> iProp Σ) E
+  Lemma sp_deposit'
+      (p1 p2: P) (b1: B) (γ: gname) (f: B → iProp Σ) E
       (exchng: storage_protocol_deposit p1 p2 b1)
       (gname_in_e: γ ∈ E)
-      : maps γ f ⊢
-          p_own γ p1 ∗ ▷ f b1 ={ E }=∗ p_own γ p2.
-   Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+      : sp_sto γ f ⊢
+          sp_own γ p1 ∗ ▷ f b1 ={ E }=∗ sp_own γ p2.
+  Proof.
     apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_deposit; trivial.
-   Qed.
+    apply sp_deposit; trivial.
+  Qed.
 
-  Lemma logic_withdraw'
-      (p1 p2: P) (b2: B) (γ: gname) (f: B -> iProp Σ) E
+  Lemma sp_withdraw'
+      (p1 p2: P) (b2: B) (γ: gname) (f: B → iProp Σ) E
       (exchng: storage_protocol_withdraw p1 p2 b2)
       (gname_in_e: γ ∈ E)
-      : maps γ f ⊢
-          p_own γ p1 ={ E }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+      : sp_sto γ f ⊢
+          sp_own γ p1 ={ E }=∗ sp_own γ p2 ∗ ▷ f b2.
+  Proof.
     apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_withdraw; trivial.
+    apply sp_withdraw; trivial.
   Qed.
 
-  Lemma logic_update'
-      (p1 p2: P) (γ: gname) (f: B -> iProp Σ) E
+  Lemma sp_update'
+      (p1 p2: P) (γ: gname) (f: B → iProp Σ) E
       (exchng: storage_protocol_update p1 p2)
       (gname_in_e: γ ∈ E)
-      : maps γ f ⊢
-          p_own γ p1 ={ E }=∗ p_own γ p2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
+      : sp_sto γ f ⊢
+          sp_own γ p1 ={ E }=∗ sp_own γ p2.
+  Proof.
     apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_update; trivial.
+    apply sp_update; trivial.
   Qed.
   
   (* SP-PointProp *)
   
-  Lemma point_prop_p_own (γ: gname) (p: P) : point_prop (p_own γ p).
+  Lemma point_prop_p_own (γ: gname) (p: P) : point_prop (sp_own γ p).
   Proof.
-    unfold p_own. apply point_prop_own.
+    rewrite sp_own_eq. unfold sp_own_def. apply point_prop_own.
   Qed.
   
   (* SP-Valid *)
   
-  Lemma p_own_valid (γ: gname) (p: P)
-      : (p_own γ p) ⊢ ⌜ ∃ q , pinv (p ⋅ q) ⌝.
+  Lemma sp_own_valid (γ: gname) (p: P)
+      : (sp_own γ p) ⊢ ⌜ ∃ q b , sp_rel (p ⋅ q) b ⌝.
   Proof.
+    rewrite sp_own_eq. unfold sp_own_def.
     iIntros "x".  iDestruct (own_valid with "x") as "%x". iPureIntro.
     generalize x. clear x.
     rewrite auth_frag_valid.
     trivial.
   Qed.
- 
+   
+  Global Instance proper_sp_own γ : Proper ((≡) ==> (⊣⊢)) (sp_own γ).
+  Proof. rewrite sp_own_eq. unfold sp_own_def. intros x y Heq.
+      setoid_rewrite Heq. trivial. Qed.
+  
+  Global Instance timeless_sp_own γ a : Timeless (sp_own γ a).
+  Proof. rewrite sp_own_eq. apply _. Qed.
+  
+  Lemma sp_own_mono γ a1 a2 : a2 ≼ a1 → sp_own γ a1 ⊢ sp_own γ a2.
+  Proof.
+    intros [t Heq]. setoid_rewrite Heq. setoid_rewrite sp_own_op.
+    iIntros "[Ha Hb]". iFrame.
+  Qed.
+  
+  Global Instance mono_sp_own' γ : Proper (flip (≼) ==> (⊢)) (sp_own γ).
+  Proof.
+    intros a1 a2. apply sp_own_mono.
+  Qed.
+  
+  Lemma sp_own_core_persistent γ a : (pcore a ≡ Some a) → Persistent (sp_own γ a).
+  Proof.
+    rewrite sp_own_eq. unfold sp_own_def.
+    intros Ha. apply own_core_persistent. apply auth_frag_core_id.
+    unfold CoreId, pcore, cmra_pcore, cmra_pcore. simpl. unfold inved_protocolUR, ucmra_pcore.
+    unfold inved_protocol_pcore.  destruct (pcore a) as [t|].
+    - inversion Ha as [x y Hb Hc Hd|]. setoid_rewrite Hb. trivial.
+    - inversion Ha.
+  Qed.
 End StorageLogic.
diff --git a/src/guarding/storage_protocol/protocol_relational.v b/src/guarding/storage_protocol/protocol_relational.v
deleted file mode 100644
index 9db6070..0000000
--- a/src/guarding/storage_protocol/protocol_relational.v
+++ /dev/null
@@ -1,1590 +0,0 @@
-From iris.algebra Require Export cmra updates.
-From iris.algebra Require Import proofmode_classes.
-From iris.algebra Require Import auth.
-From iris.prelude Require Import options.
-
-From iris.base_logic.lib Require Export own iprop.
-From iris.proofmode Require Import base.
-From iris.proofmode Require Import ltac_tactics.
-From iris.proofmode Require Import tactics.
-From iris.proofmode Require Import coq_tactics.
-
-From stdpp Require Export namespaces.
-
-(*From iris.base_logic.lib Require Export wsat.*)
-
-Require Import guarding.storage_protocol.inved.
-Require Import guarding.guard.
-Require Import guarding.internal.auth_frag_util.
-Require Import guarding.factoring_props.
-Require Import guarding.own_and_own_sep.
-Require Import guarding.internal.wsat_util.
-
-(*
-Context {Σ: gFunctors}.
-Context `{!invGS Σ}.
-*)
-
-Class InterpRel (P : Type) (B : Type) := interp_rel : P → B → Prop.
-
-
-Record StorageMixin P B
-    `{Equiv P, PCore P, Op P, Valid P, PInv P, Unit P}
-    {equ: @Equivalence P (≡)}
-    `{Equiv B, PCore B, Op B, Valid B, Unit B, InterpRel P B}
-:= {
-    protocol_mixin: ProtocolMixin P;
-    base_ra_mixin: RAMixin B; (* completely ignore core *)
-    
-    base_unit_left_id : LeftId equiv (ε : B) op;
-
-    interp_proper: Proper ((≡) ==> (≡) ==> (↔)) interp_rel;
-    interp_val: ∀ (p: P) (b: B) , interp_rel p b -> ✓ b;
-    
-    p_inv_equiv : ∀ (p: P) , pinv p ↔ ∃ b , interp_rel p b;
-}. 
-
-
-Section PropMap.
-  Context {Σ: gFunctors}.
-  
-  Context `{Equiv B, Op B, Valid B, Unit B}.
-  
-  Definition wf_prop_map (f: B -> iProp Σ) :=
-      Proper ((≡) ==> (≡)) f
-      /\ f ε ≡ (True)%I
-      /\ (∀ a b , ✓(a ⋅ b) -> f (a ⋅ b) ≡ (f a ∗ f b) % I).
-      
-  
-End PropMap.
-
-Section StorageLogic.
-  Context `{Equiv B, PCore B, Op B, Valid B, Unit B}.
-  Context `{Equiv P, PCore P, Op P, PInv P, Valid P, Unit P, InterpRel P B}.
-  
-  
-  Definition storage_protocol_guards (p: P) (b: B) :=
-      ∀ q (t: B) , interp_rel (p ⋅ q) t -> b ≼ t.
-      
-  Definition storage_protocol_exchange (p1 p2: P) (b1 b2: B)  :=
-      ∀ q t1, interp_rel (p1 ⋅ q) t1 ->
-          ∃ t2, interp_rel (p2 ⋅ q) t2
-          /\ ✓(t1 ⋅ b1)
-          /\ t1 ⋅ b1 ≡ t2 ⋅ b2.
-          
-  Definition storage_protocol_update (p1 p2: P) :=
-      ∀ q t1 , interp_rel (p1 ⋅ q) t1 -> interp_rel (p2 ⋅ q) t1.
-          
-  Definition storage_protocol_withdraw (p1 p2: P) (b2: B)  :=
-      ∀ q t1 , interp_rel (p1 ⋅ q) t1 -> ∃ t2, interp_rel (p2 ⋅ q) t2
-          /\ t1 ≡ t2 ⋅ b2.
-          
-  Definition storage_protocol_deposit (p1 p2: P) (b1: B)  :=
-      ∀ q t1 , interp_rel (p1 ⋅ q) t1 -> ∃ t2, interp_rel (p2 ⋅ q) t2
-          /\ ✓(t1 ⋅ b1)
-          /\ t1 ⋅ b1 ≡ t2.
-          
-  Definition storage_protocol_exchange_nondeterministic (p1: P) (b1: B) (output_ok: P -> B -> Prop)  :=
-      ∀ q t1 , interp_rel (p1 ⋅ q) t1 -> ∃ p2 b2 t2 , output_ok p2 b2
-          /\ interp_rel (p2 ⋅ q) t2
-          /\ ✓(t1 ⋅ b1)
-          /\ t1 ⋅ b1 ≡ t2 ⋅ b2.
-          
-  Context {equ: Equivalence (≡@{P})}.
-  Context {equb: Equivalence (≡@{B})}.
-  Context {storage_mixin: StorageMixin P B}.
-
-  Instance sm_interp_proper
-      : Proper ((≡) ==> (≡) ==> (↔)) (interp_rel).
-  Proof using storage_mixin.
-    destruct storage_mixin. trivial.
-  Qed.
-
-  Instance inved_proper
-      : Proper ((≡) ==> (≡)) (@Inved P).
-  Proof.
-    unfold Proper, "==>". intros.
-    unfold "≡", inved_protocol_equiv. trivial.
-  Qed.
-                   
-  Global Instance my_discrete : CmraDiscrete (inved_protocolR (protocol_mixin P B storage_mixin)).
-  Proof. apply discrete_cmra_discrete. Qed.
-
-  Context {Σ: gFunctors}.
-  Context `{!inG Σ (authUR (inved_protocolUR (protocol_mixin P B storage_mixin)))}.
-  Context `{!invGS Σ}.
-  
-  Definition maps (γ: gname) (f: B -> iProp Σ) : iProp Σ :=
-      ⌜ wf_prop_map f ⌝ ∗
-      own γ (◯ (Inved ε)) ∗
-      ownI γ (
-        ∃ (state_t: P * B) ,
-          own γ (● (Inved (fst state_t)))
-          ∗ ⌜ interp_rel (fst state_t) (snd state_t) ⌝
-          ∗ (f (snd state_t))
-      ). 
-     
-  Definition p_own (γ: gname) (p: P) : iProp Σ := own γ (◯ (Inved p)).
-  
-  Lemma pcore_inved_unit
-    : (pcore (Inved (ε : P)) ≡ Some (Inved ε)).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    unfold pcore, inved_protocol_pcore. destruct (pcore ε) eqn:x.
-    { destruct storage_mixin. destruct protocol_mixin0. destruct protocol_ra_mixin.
-      have k := ra_pcore_l (ε: P) p x.
-      generalize k. rewrite ra_comm. rewrite protocol_unit_left_id.
-      intro R. setoid_rewrite R. trivial.
-    }
-    trivial.
-  Qed.
-  
-  Global Instance pers_own_frag_inved_unit γ : Persistent (own γ (◯ (Inved (ε: P)))).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    apply own_core_persistent.
-    apply auth_frag_core_id.
-    unfold CoreId.
-    apply pcore_inved_unit.
-  Qed.
-  
-  Global Instance pers_maps γ f : Persistent (maps γ f).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-  apply _. Qed.
-  
-  Lemma apply_timeless (X Y Z W V : iProp Σ) (ti: Timeless Z) (ti2: Timeless W)
-      : X ∧ (Y ∗ ▷ (Z ∗ W ∗ V)) -∗ ◇ (X ∧ (Y ∗ Z ∗ W ∗ ▷ (V))).
-  Proof.
-      iIntros "l".
-      rewrite bi.except_0_and. iSplit.
-      { iDestruct "l" as "[l _]". iModIntro. iFrame. }
-      iDestruct "l" as "[_ [l [lat0 [lat1 lat2]]]]".
-      iMod "lat0" as "lat0".
-      iMod "lat1" as "lat1".
-      iModIntro. iFrame.
-  Qed.
-  
-  Lemma stuff1 (X Y Z W V : iProp Σ)
-      : (X ∧ (Y ∗ Z ∗ W ∗ V)) ⊢ W.
-  Proof.
-    iIntros "x". iDestruct "x" as "[_ [_ [_ [w _]]]]". iFrame.
-  Qed.
-  
-  Lemma incl_of_inved_incl_assumes_unital (p1 p2 : P)
-    (incll :
-      @included (InvedProtocol P) (inved_protocol_equiv P) (inved_protocol_op P)
-      (Inved p1) (Inved p2)) : p1 ≼ p2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    unfold "≼" in incll. destruct incll as [z incll].
-    destruct z.
-    - unfold "⋅", inved_protocol_op, "≡", inved_protocol_equiv in incll.
-      unfold "≼". exists ε.
-      setoid_rewrite (@comm P).
-      + destruct storage_mixin. destruct protocol_mixin0.
-          setoid_rewrite incll.
-          unfold LeftId in protocol_unit_left_id.
-          symmetry.
-          apply protocol_unit_left_id.
-      + destruct storage_mixin. destruct protocol_mixin0. destruct protocol_ra_mixin.
-          apply ra_comm.
-   - unfold "≡", inved_protocol_equiv, "⋅", inved_protocol_op in incll.
-      unfold "≼". exists p. trivial.
-  Qed.
-  
-  Lemma auth_frag_conjunct_to_incl (γ: gname) (p state: P) (W: iProp Σ)
-      : own γ (◯ Inved p) ∧ (own γ (● Inved state) ∗ W) ⊢ ⌜ p ≼ state ⌝. 
-  Proof.
-    iIntros "x".
-    iAssert (((own γ (● Inved state)) ∧ (own γ (◯ Inved p)))%I) with "[x]" as "t".
-    { iSplit. 
-        { iDestruct "x" as "[_ [x _]]". iFrame. }
-        { iDestruct "x" as "[x _]". iFrame. }
-    }
-    iDestruct (auth_frag_conjunct with "t") as "%incll".
-    iPureIntro.
-    apply incl_of_inved_incl_assumes_unital. trivial.
-  Qed.
-  
-  (* SP-Guard *)
-  
-  Lemma logic_guard (p: P) (b: B) (γ: gname) (E: coPset) (f: B -> iProp Σ)
-    (g: storage_protocol_guards p b)
-    (is_in: γ ∈ E)
-    : maps γ f ⊢ (p_own γ p &&{ E }&&> ▷ f b).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps. iIntros "[%wfm [#ounit #oinv]]".
-    iDestruct (guards_from_inv _ _ E with "oinv") as "mg". { set_solver. }
-    assert (Inhabited (P * B)) as IP. { apply populate. apply (ε, ε). }
-    rewrite bi.later_exist.
-    iDestruct (guards_true E (p_own γ p)) as "gt".
-    iDestruct (guards_transitive _ (p_own γ p) True%I with "[gt mg]") as "gg".
-      { iFrame "gt". iFrame "mg". }
-    iDestruct (lguards_exists_with_lhs (P*B) (p_own γ p) 
-      (λ (state_t: P*B), (▷ (⌜ p ≼ state_t.1 ⌝))%I)
-      (λ (state_t: P*B), (▷ (own γ (● Inved state_t.1) ∗ ⌜interp_rel state_t.1 state_t.2⌝ ∗ f state_t.2))%I)
-      E 0
-      with "[gg]") as "ggg".
-    {
-      iIntros (x) "o". unfold p_own. iNext. iDestruct (auth_frag_conjunct_to_incl with "o") as "o"; trivial.
-    }
-    { unfold guards. iFrame "gg". }
-    assert ((∃ x, ▷ (own γ (● Inved x.1) ∗ ⌜interp_rel x.1 x.2⌝ ∗ f x.2) ∗ ▷ ⌜p ≼ x.1⌝)
-      ⊣⊢ (▷ f b ∗ ▷(f b -∗ ∃ x, (own γ (● Inved x.1) ∗ ⌜interp_rel x.1 x.2⌝ ∗ f x.2) ∗ ⌜p ≼ x.1⌝)))
-      as Equ.
-    { iIntros. iSplit. { iIntros "r".
-      rewrite <- bi.later_sep. iNext.
-      iDestruct "r" as (state) "[[r [%pi t]] %p_incl_x]".
-      unfold storage_protocol_guards in g.
-      have p_incl_x_copy := p_incl_x.
-      unfold "≼" in p_incl_x. destruct p_incl_x as [z p_incl_x].
-      assert (interp_rel (p ⋅ z) state.2) as pinv_pz.
-          { destruct storage_mixin. destruct protocol_mixin0. setoid_rewrite <- p_incl_x. trivial. }
-      have b_le_interp := g z (state.2) pinv_pz.
-      destruct b_le_interp as [bz b_le_interp].
-      
-      unfold wf_prop_map in wfm.
-      destruct wfm as [fprop [funit fop]].
-
-      assert (✓ (b ⋅ bz)) as is_val.
-      { destruct storage_mixin. destruct base_ra_mixin0.
-          setoid_rewrite <- b_le_interp.
-          apply interp_val0 with (p := p ⋅ z). trivial. }
-          
-      setoid_rewrite b_le_interp.
-      setoid_rewrite fop; trivial.
-
-      iDestruct "t" as "[fb fbz]".
-      iFrame "fb".
-      iIntros "fb".
-      iExists state.
-      
-      setoid_rewrite b_le_interp.
-      setoid_rewrite fop; trivial.
-      iFrame. iSplit; iPureIntro; trivial.
-      setoid_rewrite p_incl_x. setoid_rewrite <- b_le_interp.
-      trivial.
-    }
-    { iIntros "[a b]". 
-      iDestruct ("b" with "a") as "b".
-      rewrite bi.later_exist.
-      iDestruct "b" as (state) "b". iExists state.
-      rewrite bi.later_sep. iFrame.
-    } }    
-    setoid_rewrite Equ.
-    iApply guards_weaken_rhs_l. iFrame "ggg".
-  Qed.
-   
-  Lemma own_sep_inv_incll_helper_nondet (p1 st : P) (t1 : B) (output_ok : P -> P -> Prop)
-    (cond : ∀ (q : P) , interp_rel (p1 ⋅ q) t1 → ∃ p2 t2 , output_ok p2 q /\ interp_rel (p2 ⋅ q) t2)
-   : ∀ (z: InvedProtocol P) , interp_rel st t1 -> ✓ (Inved st) -> Inved p1 ⋅ z ≡ Inved st →
-    ∃ p2 , output_ok p2 (match z with Inved z0 => z0 | Nah => ε end) /\ ✓ (Inved p2 ⋅ z).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 storage_mixin Σ.
-  intros z inv v eq.
-    destruct z.
-    - unfold "⋅", inved_protocol_op.
-      unfold "⋅", inved_protocol_op in eq.
-      unfold "≡", inved_protocol_equiv in eq.
-      unfold "✓", inved_protocol_valid. 
-      
-      setoid_rewrite <- eq in v.
-      {
-        unfold "✓", inved_protocol_valid in v. 
-        destruct v as [v pi].
-        assert (p1 ⋅ (@ε _ H9) ≡ p1) as eq2.
-        { destruct storage_mixin. destruct protocol_mixin0.
-            destruct protocol_ra_mixin.
-            rewrite ra_comm.
-            apply protocol_unit_left_id.
-        }
-        assert (interp_rel (p1 ⋅ (@ε _ H9)) t1) as pi2.
-        {
-          destruct storage_mixin.
-          destruct protocol_mixin0.
-          unfold Proper, "==>", impl in interp_proper0.
-          rewrite <- interp_proper0 with (x := st). { apply inv. }
-          { symmetry. setoid_rewrite <- eq. trivial. }
-          trivial.
-        }
-        have c := cond (@ε _ H9) pi2.
-        destruct c as [p2 [b [oo c]]].
-        exists p2.
-        split. { apply oo. }
-        exists ε.
-        trivial.
-        rewrite p_inv_equiv; trivial. exists b. apply c.
-      }
-      { destruct storage_mixin. trivial. }
-    - unfold "⋅", inved_protocol_op in eq.
-      unfold "≡", inved_protocol_equiv in eq.
-      unfold "⋅", inved_protocol_op.
-      
-      setoid_rewrite <- eq in v.
-      {
-        unfold "✓", inved_protocol_valid in v.
-        unfold "✓", inved_protocol_valid.
-        destruct v as [v pi].
-        
-        assert (interp_rel (p1 ⋅ p) t1) as pinv1. {
-          destruct storage_mixin.
-          destruct protocol_mixin0.
-          unfold Proper, "==>", impl in interp_proper0.
-          rewrite <- interp_proper0. { apply inv. }
-          { symmetry. trivial. } trivial.
-        }
-        have c := cond p pinv1.
-        destruct c as [p2 [b [oo c]]].
-        exists p2.
-        split; trivial.
-        exists ε.
-        
-        destruct storage_mixin.
-        destruct protocol_mixin0.
-        unfold Proper, "==>", impl in inv_proper.
-        assert (p2 ⋅ p ⋅ (@ε _ H9) ≡ p2 ⋅ p) as eq2.
-        { destruct storage_mixin. destruct protocol_mixin0.
-            destruct protocol_ra_mixin.
-            rewrite ra_comm.
-            apply protocol_unit_left_id.
-        }
-        apply inv_proper with (x := p2 ⋅ p); trivial.
-        rewrite p_inv_equiv; trivial. exists b. apply c.
-      }
-      { destruct storage_mixin. trivial. }
-  Qed.
-  
-  (*
-  Lemma own_sep_inv_incll_helper (p1 p2 st : P)
-    (cond : ∀ q : P, pinv (p1 ⋅ q) → pinv (p2 ⋅ q))
-   : ∀ (z: InvedProtocol P) , ✓ (Inved st) -> Inved p1 ⋅ z ≡ Inved st → ✓ (Inved p2 ⋅ z).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    intros z v eq.
-    destruct z.
-    - unfold "⋅", inved_protocol_op.
-      unfold "⋅", inved_protocol_op in eq.
-      unfold "≡", inved_protocol_equiv in eq.
-      unfold "✓", inved_protocol_valid. 
-      
-      setoid_rewrite <- eq in v.
-      {
-        unfold "✓", inved_protocol_valid in v. 
-        destruct v as [v pi].
-        have c := cond v pi.
-        exists v.
-        trivial.
-      }
-      { destruct storage_mixin. trivial. }
-    - unfold "⋅", inved_protocol_op in eq.
-      unfold "≡", inved_protocol_equiv in eq.
-      unfold "⋅", inved_protocol_op.
-      
-      setoid_rewrite <- eq in v.
-      {
-        unfold "✓", inved_protocol_valid in v.
-        unfold "✓", inved_protocol_valid.
-        destruct v as [v pi].
-        
-        assert (pinv (p1 ⋅ (p ⋅ v))) as pinv1. {
-          destruct storage_mixin.
-          destruct protocol_mixin0.
-          unfold Proper, "==>", impl in inv_proper.
-          apply inv_proper with (x := p1 ⋅ p ⋅ v); trivial.
-          destruct protocol_ra_mixin.
-          symmetry.
-          apply ra_assoc.
-        }
-        have c := cond (p ⋅ v) pinv1.
-        exists v.
-        
-        destruct storage_mixin.
-        destruct protocol_mixin0.
-        unfold Proper, "==>", impl in inv_proper.
-        apply inv_proper with (x := p2 ⋅ (p ⋅ v)); trivial.
-        destruct protocol_ra_mixin.
-        apply ra_assoc.
-      }
-      { destruct storage_mixin. trivial. }
-  Qed.
-  *)
-        
-  Lemma op_nah (p1 state : P)
-    : Inved p1 ⋅ Nah ≡ Inved state -> p1 ≡ state.
-  Proof. intros. trivial. Qed.
-  
-  Lemma op_inved_inved (p1 p2 p : P)
-    : Inved p1 ⋅ Inved p2 ≡ Inved p -> p1 ⋅ p2 ≡ p.
-  Proof. intros. trivial. Qed.
-        
-  (*
-  Lemma own_sep_inv_incll γ (p1 p2 state : P)
-      (cond: ∀ q , pinv (p1 ⋅ q) -> pinv (p2 ⋅ q))
-    : own γ (◯ Inved p1) ∗ own γ (● Inved state) ==∗
-      ∃ (z: P) , ⌜ state ≡ p1 ⋅ z ⌝ ∗ own γ (◯ Inved p2) ∗ own γ (● Inved (p2 ⋅ z)).
-  Proof.
-    iIntros "[x y]".
-    iDestruct (own_valid with "y") as "%val".
-    iMod (own_sep_auth_incll γ (Inved p1) (Inved p2) (Inved state) with "[x y]") as "x".
-    {
-      intro.
-      apply own_sep_inv_incll_helper; trivial.
-      generalize val. rewrite auth_auth_valid. trivial.
-    }
-    { iFrame. }
-    iDestruct "x" as (z) "[%eq [frag auth]]".
-    destruct z.
-    {
-      have eq0 := op_nah _ _ eq.
-      assert (Inved p2 ⋅ Nah ≡ Inved p2) as eq1 by trivial.
-      setoid_rewrite eq1.
-      iExists (ε:P).
-      assert (p2 ⋅ ε ≡ p2) as eq2.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
-      }
-      setoid_rewrite eq2.
-      iFrame.
-      iPureIntro.
-      assert (p1 ⋅ ε ≡ p1) as eq3.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
-      }
-      setoid_rewrite eq3. symmetry. trivial.
-    }
-    {
-      iExists p.
-      
-      assert (Inved p2 ⋅ Inved p ≡ Inved (p2 ⋅ p)) as eq0 by trivial.
-      setoid_rewrite eq0.
-      iFrame.
-      iPureIntro. symmetry. apply op_inved_inved. trivial.
-    }
-   Qed.
-   *)
-   
-   Lemma own_sep_inv_incll_nondet γ (p1 state : P) (t1: B) (output_ok: P -> P -> Prop)
-      (cond: ∀ q , interp_rel (p1 ⋅ q) t1 -> ∃ p2 t2 , output_ok p2 q /\ interp_rel (p2 ⋅ q) t2)
-      (pi: interp_rel state t1)
-    : own γ (◯ Inved p1) ∗ own γ (● Inved state) ==∗
-      ∃ (z p2: P) , ⌜ output_ok p2 z /\ state ≡ p1 ⋅ z ⌝
-          ∗ own γ (◯ Inved p2) ∗ own γ (● Inved (p2 ⋅ z)).
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 storage_mixin Σ.
-   iIntros "[x y]".
-   iDestruct (own_valid with "y") as "%val".
-    iMod (own_sep_auth_incll_nondet γ (Inved p1) (Inved state)
-    (λ p q , match p with
-      | Inved a => output_ok a (match q with Inved b => b | Nah => ε end)
-      | Nah => False
-    end)
-     with "[x y]") as "x".
-    {
-      intro. intro equi.
-      assert (✓ Inved state) as val2. { generalize val. rewrite auth_auth_valid. trivial. }
-      have rr := own_sep_inv_incll_helper_nondet p1 state t1 output_ok cond z pi val2 equi.
-      destruct rr as [p2 [rr v]]. exists (Inved p2). split; trivial.
-    }
-    { iFrame. }
-    iDestruct "x" as (z p2) "[%eq [frag auth]]".
-    destruct eq as [big_oo eq].
-    destruct p2. { intuition. }
-    rename p into p2.
-    destruct z.
-    {
-      have eq0 := op_nah _ _ eq.
-      assert (Inved p2 ⋅ Nah ≡ Inved p2) as eq1 by trivial.
-      setoid_rewrite eq1.
-      iExists (ε:P).
-      assert (p2 ⋅ ε ≡ p2) as eq2.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
-      }
-      iModIntro. iExists p2.
-      setoid_rewrite eq2.
-      iFrame.
-      iPureIntro.
-      split. { trivial. }
-      assert (p1 ⋅ ε ≡ p1) as eq3.
-      { destruct storage_mixin. destruct protocol_mixin0.
-          destruct protocol_ra_mixin.
-          rewrite ra_comm.
-          apply protocol_unit_left_id.
-      }
-      setoid_rewrite eq3. symmetry. trivial.
-    }
-    {
-      iExists p.
-      
-      assert (Inved p2 ⋅ Inved p ≡ Inved (p2 ⋅ p)) as eq0 by trivial.
-      setoid_rewrite eq0.
-      iModIntro. iExists p2. iFrame.
-      iPureIntro. split. { apply big_oo. } symmetry. apply op_inved_inved. trivial.
-    }
-   Qed.
-   
-  Lemma own_inved_op_both (a b: P) γ :
-      own γ (◯ Inved a) ∗ own γ (◯ Inved b) ⊣⊢ own γ (◯ Inved (a ⋅ b)).
-  Proof.
-    rewrite <- own_op.
-    replace (◯ Inved a ⋅ ◯ Inved b) with (@auth_frag
-          (@inved_protocolUR P H4 H5 H6 H7 H8 H9 equ
-             (@protocol_mixin P B H4 H5 H6 H8 H7 H9 equ H H0 H1 H2 H3 H10 storage_mixin))
-          (@Inved P (@op P H6 a b))); trivial.
-  Qed.
-          
-  Lemma own_inved_op (a b: P) γ :
-      own γ (◯ Inved a) ∗ own γ (◯ Inved b) ⊢ own γ (◯ Inved (a ⋅ b)).
-  Proof. rewrite own_inved_op_both. trivial. Qed.
-      
-  Lemma own_inved_op_split (a b: P) γ :
-      own γ (◯ Inved (a ⋅ b)) ⊢ own γ (◯ Inved a) ∗ own γ (◯ Inved b).
-  Proof. rewrite own_inved_op_both. trivial. Qed.
-    
-  (*
-  Lemma logic_exchange
-    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ)
-    (exchng: storage_protocol_exchange p1 p2 b1 b2)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[%wfm [#ounit #m]] [p f]".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
-    { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state) "lat".
-    iDestruct "lat" as "[ois [ps fi]]".
-    iMod "ois" as "ois".
-    iMod "ps" as "%ps".
-    unfold p_own.
-    iMod (own_sep_inv_incll γ p1 p2 state with "[p ois]") as (z) "[%incll [p ois]]".
-    { unfold storage_protocol_exchange in exchng. intros q pi.
-        have exch := exchng q pi. intuition. }
-    { iFrame. }
-    
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state)
-          ≡ f(interp (p1 ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    have exch := exchng z pinv_p1_z.
-    destruct exch as [pinv_p2_z [val_interp1 interp_eq]].
-    assert (✓ (interp (p2 ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[ois fi]"
-          as "inv_to_return".
-    {
-      iModIntro. (* strip later *)
-      iExists (p2 ⋅ z). iFrame "ois". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
-    { iFrame "m". iFrame "inv_to_return". iFrame "w". iFrame "od". }
-    iModIntro. iModIntro. iFrame.
-  Qed.
-  *)
-   
-  Lemma logic_exchange_nondeterministic
-    (p1: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ)
-    (exchng: storage_protocol_exchange_nondeterministic p1 b1 output_ok)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗
-          ∃ p2 b2 , ⌜ output_ok p2 b2 ⌝ ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[%wfm [#ounit #m]] [p f]".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
-    { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state_t) "lat".
-    iDestruct "lat" as "[ois [ps fi]]".
-    iMod "ois" as "ois".
-    iMod "ps" as "%ps".
-    unfold p_own.
-    iMod (own_sep_inv_incll_nondet γ p1 state_t.1 state_t.2 (λ p2 q , ∃ b2 t2 , output_ok p2 b2
-          /\ interp_rel (p2 ⋅ q) t2
-          /\ ✓(state_t.2 ⋅ b1)
-          /\ state_t.2 ⋅ b1 ≡ t2 ⋅ b2) with "[p ois]")
-        as (z p2) "[[%big_output_ok %incll] [p ois]]".
-    { unfold storage_protocol_exchange in exchng. intros q pi.
-        have exch := exchng q state_t.2 pi. destruct exch as [p2 [b2 [t2 exch]]]. exists p2. exists t2. intuition. exists b2. exists t2. intuition. }
-    { trivial. }
-    { iFrame. }
-    destruct big_output_ok as [b2 [t2 [oo [pix [vix interp_eq]]]]].
-    
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    (*assert (f (interp state)
-          ≡ f(interp (p1 ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }*)
-    
-    (*setoid_rewrite equiv_interp_state.*)
-    
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-        rewrite p_inv_equiv; trivial. exists (state_t.2). apply ps.
-    }
-
-    assert (✓ (t2 ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ (state0_t0 : P * B),
-          own γ (● Inved state0_t0.1) ∗ ⌜interp_rel state0_t0.1 state0_t0.2⌝ ∗ f state0_t0.2)%I)
-          with "[ois fi]"
-          as "inv_to_return".
-    {
-      iModIntro. (* strip later *)
-      iExists (p2 ⋅ z, t2). iFrame "ois". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
-    { iFrame "m". iFrame "inv_to_return". iFrame "w". iFrame "od". }
-    iModIntro. iModIntro. iFrame.
-    iPureIntro. apply oo.
-  Qed.
-   
-  (* SP-Exchange *)
-   
-  Lemma logic_exchange
-    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ)
-    (exchng: storage_protocol_exchange p1 p2 b1 b2)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "x y".
-    iDestruct (logic_exchange_nondeterministic p1 b1 (λ p b, p = p2 ∧ b = b2) γ f with "x y") as "J".
-    { unfold storage_protocol_exchange in exchng.
-      unfold storage_protocol_exchange_nondeterministic.
-      intros q t1 pi. exists p2. exists b2.
-      have ex := exchng q t1 pi. destruct ex as [t2 ex]. exists t2. intuition.
-    }
-    iMod "J" as (p0 b0) "[[%eq1 %eq2] t]". iModIntro. rewrite eq1. rewrite eq2. iFrame.
-  Qed.
-   
-   (*
-  Lemma logic_exchange_with_extra_guard
-    (p1 p2 q: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ)
-    (exchng: storage_protocol_exchange (p1 ⋅ q) (p2 ⋅ q) b1 b2)
-    : maps γ f ∗ □ (G &&{ {[ γ ]} }&&$> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[[%wfm [#ounit #m]] [#gu #kbi]] [g [p f]]".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
-    { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state) "lat".
-    unfold fguards, guards_with.
-    iDestruct ("gu" $! G) as "gu2".
-    
-    iDestruct ("gu2" with "[g lat]") as "gu3".
-    { iFrame "g". iIntros "g". iFrame "g".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iExists ((∃ state0 : P, own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I).
-        iFrame "m".
-        setoid_rewrite know_bulk_inv_singleton. unfold know_inv.
-        iModIntro. iExists state. iFrame "lat".
-    }
-    
-    iMod "gu3" as "[po b]".
-    
-     iAssert ((own γ (◯ Inved q) ∧
-          (◇ ∃ state : P, G ∗ ▷
-                (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state))))%I)
-          with "[po b]" as "x".
-      { iSplit. { iFrame. } 
-        iDestruct ("b" with "po") as "[ex t]".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iDestruct "ex" as (P0) "[#own lat]".
-        iDestruct (ownIagree γ P0 _ with "[m own]") as "eq".
-        { iSplitL. { iFrame "own". } iFrame "m". }
-        iRewrite "eq" in "lat".
-        iMod (bi.later_exist_except_0 with "lat") as (state0) "lat".
-        iExists state0. iFrame.
-      }
-      iMod (and_except0_r with "x") as "x".
-      rewrite bi.and_exist_l.
-      iDestruct "x" as (state0) "x".
-      iMod (apply_timeless with "x") as "x".
-      iDestruct (stuff1 with "x") as "%pinvs".
-      unfold p_own.
-      (*iDestruct (stuff3 γ p1 q state0 with "[p x]") as "%incll". { iFrame. }*)
-      
-      iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0) ∗ (G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)))%I with "[x]" as "x".
-      { iSplit. { iDestruct "x" as "[x _]". iFrame. }
-          iDestruct "x" as "[_ [x [y z]]]". iFrame. }
-      iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
-      { apply auth_frag_disjointness. }
-      iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)) with "[y]") as "[y z]".
-      { iFrame "y". iIntros "[k _]". iFrame. }
-      
-      iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-      iMod (own_sep_inv_incll γ (p1 ⋅ q) (p2 ⋅ q) state0 with "[own_p_q x]")
-          as (z) "[%incll [own_p_q x]]".
-      { unfold storage_protocol_exchange in exchng.
-        intro q0. have exq := exchng q0. intuition. }
-      { iFrame. }
-      
-      iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-      iDestruct ("z" with "q") as "[_ z]".
-       
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    iDestruct "z" as "[g [_ fi]]".
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    have exch := exchng z pinv_p1_z.
-    destruct exch as [pinv_p2_z [val_interp1 interp_eq]].
-    assert (✓ (interp (p2 ⋅ q ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[x fi]"
-          as "inv_to_return".
-    {
-      iModIntro. (* strip later *)
-      iExists (p2 ⋅ q ⋅ z). iFrame "x". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
-    { iFrame "m". iFrame "inv_to_return". iFrame "w". iFrame "od". }
-    iModIntro. iModIntro. iFrame.
-  Qed.
-  *)
-  
-  (*
-  Lemma logic_exchange_with_extra_guard_nondeterministic
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ)
-    (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
-    : maps γ f ∗ □ (G &&{ {[ γ ]} }&&$> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[[%wfm [#ounit #m]] [#gu #kbi]] [g [p f]]".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iDestruct (ownI_open with "[w m oe]") as "[w [latp od]]".
-    { iFrame "w". iFrame "m". iFrame "oe". }
-    iMod (bi.later_exist_except_0 with "latp") as (state) "lat".
-    unfold fguards, guards_with.
-    iDestruct ("gu" $! G) as "gu2".
-    
-    iDestruct ("gu2" with "[g lat]") as "gu3".
-    { iFrame "g". iIntros "g". iFrame "g".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iExists ((∃ state0 : P, own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I).
-        iFrame "m".
-        setoid_rewrite know_bulk_inv_singleton. unfold know_inv.
-        iModIntro. iExists state. iFrame "lat".
-    }
-    
-    iMod "gu3" as "[po b]".
-    
-     iAssert ((own γ (◯ Inved q) ∧
-          (◇ ∃ state : P, G ∗ ▷
-                (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state))))%I)
-          with "[po b]" as "x".
-      { iSplit. { iFrame. } 
-        iDestruct ("b" with "po") as "[ex t]".
-        setoid_rewrite storage_bulk_inv_singleton. unfold storage_inv.
-        iDestruct "ex" as (P0) "[#own lat]".
-        iDestruct (ownIagree γ P0 _ with "[m own]") as "eq".
-        { iSplitL. { iFrame "own". } iFrame "m". }
-        iRewrite "eq" in "lat".
-        iMod (bi.later_exist_except_0 with "lat") as (state0) "lat".
-        iExists state0. iFrame.
-      }
-      iMod (and_except0_r with "x") as "x".
-      rewrite bi.and_exist_l.
-      iDestruct "x" as (state0) "x".
-      iMod (apply_timeless with "x") as "x".
-      iDestruct (stuff1 with "x") as "%pinvs".
-      unfold p_own.
-      (*iDestruct (stuff3 γ p1 q state0 with "[p x]") as "%incll". { iFrame. }*)
-      
-      iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0) ∗ (G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)))%I with "[x]" as "x".
-      { iSplit. { iDestruct "x" as "[x _]". iFrame. }
-          iDestruct "x" as "[_ [x [y z]]]". iFrame. }
-      iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
-      { apply auth_frag_disjointness. }
-      iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ G ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)) with "[y]") as "[y z]".
-      { iFrame "y". iIntros "[k _]". iFrame. }
-      
-      iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-      iMod (own_sep_inv_incll_nondet γ (p1 ⋅ q) state0 (λ p2_q r , ∃ p2 b2 , p2_q = p2 ⋅ q /\ output_ok p2 b2
-          /\ pinv ((p2 ⋅ q) ⋅ r)
-          /\ ✓(interp ((p1 ⋅ q) ⋅ r) ⋅ b1)
-          /\ interp ((p1 ⋅ q) ⋅ r) ⋅ b1 ≡ interp ((p2 ⋅ q) ⋅ r) ⋅ b2) with "[own_p_q x]")
-          as (z p2_q) "[%incll [own_p_q x]]".
-      { unfold storage_protocol_exchange_nondeterministic in exchng.
-        intro r. intro j0. have exq := exchng r j0.
-        destruct exq as [p2_q [b2 exq]].
-        destruct exq as [[p2 [eq oo]] [a b]].
-        exists (p2 ⋅ q). split.
-        { exists p2. exists b2. intuition. { rewrite <- eq. apply a. }
-            rewrite <- eq. trivial. }
-        { rewrite <- eq. apply a. }
-      }
-      { apply pinvs. }
-      { iFrame. }
-      
-      destruct incll as [[p2 [b2 [p2_q_eq bigconj]]] incll].
-      rewrite p2_q_eq.
-      iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-      iDestruct ("z" with "q") as "[_ z]".
-      
-      destruct bigconj as [oo [pix [iix interp_eq]]].
-       
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    iDestruct "z" as "[g [_ fi]]".
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    assert (✓ (interp (p2 ⋅ q ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[x fi]"
-          as "inv_to_return".
-    {
-      iModIntro. (* strip later *)
-      iExists (p2 ⋅ q ⋅ z). iFrame "x". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct (ownI_close γ _ with "[w m inv_to_return od]") as "[w en]".
-    { iFrame "m". iFrame "inv_to_return". iFrame "w". iFrame "od". }
-    iModIntro. iModIntro. iFrame. iExists p2. iExists b2. iFrame. iPureIntro. trivial.
-  Qed.
-  *)
-  
-  (*
-  Lemma logic_exchange_with_extra_guard_nondeterministic2
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ) E
-    (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
-    (gname_in_e: γ ∈ E)
-    : maps γ f ∗ □ (G &&{ E }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ E }=∗ ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[[%wfm [#ounit #m]] #gu] [g [p f]]".
-    iDestruct (guards_from_inv _ _ E with "m") as "mg". { set_solver. }
-    iDestruct (guards_true E G) as "gt".
-    iDestruct (guards_transitive _ G True%I with "[gt mg]") as "gg".
-    { iFrame "gt". iFrame "mg". }
-    iDestruct (guards_open_two_simultaneously G _ _ E E with "[g gg gu]") as "opened".
-    { set_solver. }
-    { iFrame "g". iSplit. { iFrame "gg". } iFrame "gu". }
-    iMod "opened" as (T) "[t [tinv [town back]]]".
-    
-    iAssert ((◇ own γ (◯ Inved q) ∧ (
-          ◇ (▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T)
-          ∗
-          ◇ (∃ state : P, ▷
-                (own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)))
-          ))%I)
-          with "[t tinv town]" as "x".
-    { iSplit. { iMod ("town" with "t") as "town". unfold p_own.
-        iDestruct "town" as "[x y]". iModIntro. iFrame "x". }
-        iDestruct ("tinv" with "t") as "[tinv back]".
-        iFrame "back".
-        iMod "tinv" as "tinv".
-        iMod (bi.later_exist_except_0 with "tinv") as (state0) "tinv".
-        iModIntro.
-        iExists state0.
-        iFrame "tinv".
-    }
-    
-    rewrite <- bi.except_0_sep.
-    rewrite <- bi.except_0_and.
-    iMod "x" as "x".
-    
-    rewrite bi.sep_exist_l.
-    rewrite bi.and_exist_l.
-    iDestruct "x" as (state0) "x".
-    iMod (apply_timeless with "x") as "x".
-    iDestruct (stuff1 with "x") as "%pinvs".
-    unfold p_own.
-    
-    iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0) ∗ ((▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T) ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)))%I with "[x]" as "x".
-      { iSplit. { iDestruct "x" as "[x _]". iFrame. }
-          iDestruct "x" as "[_ [x [y z]]]". iFrame. }
-          
-    iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
-      { apply auth_frag_disjointness. }
-      
-    iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ (▷ (∃ state : P, own γ (● Inved state) ∗ ⌜pinv state⌝ ∗ f (interp state)) -∗ T) ∗ ⌜pinv state0⌝ ∗ ▷ f (interp state0)) with "[y]") as "[y z]".
-      { iFrame "y". iIntros "[k _]". iFrame. }
-      
-    iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-    iMod (own_sep_inv_incll_nondet γ (p1 ⋅ q) state0 (λ p2_q r , ∃ p2 b2 , p2_q = p2 ⋅ q /\ output_ok p2 b2
-          /\ pinv ((p2 ⋅ q) ⋅ r)
-          /\ ✓(interp ((p1 ⋅ q) ⋅ r) ⋅ b1)
-          /\ interp ((p1 ⋅ q) ⋅ r) ⋅ b1 ≡ interp ((p2 ⋅ q) ⋅ r) ⋅ b2) with "[own_p_q x]")
-          as (z p2_q) "[%incll [own_p_q x]]".
-      { unfold storage_protocol_exchange_nondeterministic in exchng.
-        intro r. intro j0. have exq := exchng r j0.
-        destruct exq as [p2_q [b2 exq]].
-        destruct exq as [[p2 [eq oo]] [a b]].
-        exists (p2 ⋅ q). split.
-        { exists p2. exists b2. intuition. { rewrite <- eq. apply a. }
-            rewrite <- eq. trivial. }
-        { rewrite <- eq. apply a. }
-      }
-      { apply pinvs. }
-      { iFrame. }
-      
-      destruct incll as [[p2 [b2 [p2_q_eq bigconj]]] incll].
-      rewrite p2_q_eq.
-      iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-      iDestruct ("z" with "q") as "[_ z]".
-      
-      destruct bigconj as [oo [pix [iix interp_eq]]].
-       
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }
-    
-    iDestruct "z" as "[g [_ fi]]".
-    setoid_rewrite equiv_interp_state.
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. trivial.
-    }
-
-    assert (✓ (interp (p2 ⋅ q ⋅ z) ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0 : P,
-          own γ (● Inved state0) ∗ ⌜pinv state0⌝ ∗ f (interp state0))%I)
-          with "[x fi]"
-          as "inv_to_return".
-    {
-      iModIntro.
-      iExists (p2 ⋅ q ⋅ z). iFrame "x". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct ("g" with "inv_to_return") as "g".
-    iMod ("back" with "g") as "g".
-    iModIntro. iFrame. iExists p2. iExists b2. iFrame. iPureIntro. trivial.
-  Qed.
-  *)
-    
-  Lemma logic_exchange_with_extra_guard_nondeterministic_with_later
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ) E n
-    (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
-    (gname_in_e: γ ∈ E)
-    : maps γ f ∗ (G &&{ E ; n }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ E, ∅ }=∗ ▷^n (|={ ∅, E }=> ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[[%wfm [#ounit #m]] #gu] [g [p f]]".
-    iDestruct (guards_from_inv _ _ E with "m") as "mg". { set_solver. }
-    iDestruct (guards_true E G) as "gt".
-    iDestruct (guards_transitive _ G True%I with "[gt mg]") as "gg".
-    { iFrame "gt". iFrame "mg". }
-    iDestruct (lguards_weaken_later _ _ _ 0 n with "[gg]") as "ggg". { lia. }
-    { iFrame "gg". }
-    iDestruct (lguards_open_two_simultaneously G _ _ E E n with "[g ggg gu]") as "opened".
-    { set_solver. }
-    { iFrame "g". iSplit. { iFrame "ggg". } iFrame "gu". }
-    iMod "opened" as (T) "[t [tinv [town back]]]".
-    
-    iAssert ((▷^n (◇ own γ (◯ Inved q) ∧ (
-          ◇ (▷ (∃ state_t : (P * B), own γ (● Inved state_t.1) ∗ ⌜interp_rel state_t.1 state_t.2⌝ ∗ f state_t.2) -∗ T)
-          ∗
-          ◇ (∃ state_t : (P * B), ▷
-                (own γ (● Inved state_t.1) ∗ ⌜interp_rel state_t.1 state_t.2⌝ ∗ f state_t.2))
-          )))%I)
-          with "[t tinv town]" as "x".
-    { iSplit. { iDestruct ("town" with "t") as "town". iNext. unfold p_own.
-        iDestruct "town" as "[x y]". iFrame "x". }
-        iDestruct ("tinv" with "t") as "[tinv back]".
-        iFrame "back". iNext. iMod "tinv" as "tinv".
-        iMod (bi.later_exist_except_0 with "tinv") as (state0) "tinv".
-        iModIntro. iExists state0. iFrame "tinv".
-    }
-    
-    replace (E ∖ E) with (@empty coPset coPset_empty) by set_solver.
-    iModIntro. iNext.
-    
-    rewrite <- bi.except_0_sep.
-    rewrite <- bi.except_0_and.
-    iMod "x" as "x".
-    
-    rewrite bi.sep_exist_l.
-    rewrite bi.and_exist_l.
-    iDestruct "x" as (state0) "x".
-    iMod (apply_timeless with "x") as "x".
-    iDestruct (stuff1 with "x") as "%pinvs".
-    unfold p_own.
-    
-    iAssert (own γ (◯ Inved q) ∧ own γ (● Inved state0.1) ∗ ((▷ (∃ state_t : P * B, own γ (● Inved state_t.1) ∗ ⌜interp_rel state_t.1 state_t.2⌝ ∗ f state_t.2) -∗ T) ∗ ⌜interp_rel state0.1 state0.2⌝ ∗ ▷ f state0.2))%I with "[x]" as "x".
-      { iSplit. { iDestruct "x" as "[x _]". iFrame. }
-          iDestruct "x" as "[_ [x [y z]]]". iFrame. }
-          
-    iDestruct (andsep_to_sepand_ucmra with "x") as "[x y]".
-      { apply auth_frag_disjointness. }
-      
-    iDestruct (own_separates_out γ (◯ Inved q) (own γ (◯ Inved q) ∧ (▷ (∃ state_t : P * B, own γ (● Inved state_t.1) ∗ ⌜interp_rel state_t.1 state_t.2⌝ ∗ f state_t.2) -∗ T) ∗ ⌜interp_rel state0.1 state0.2⌝ ∗ ▷ f state0.2) with "[y]") as "[y z]".
-      { iFrame "y". iIntros "[k _]". iFrame. }
-      
-    iDestruct (own_inved_op p1 q γ with "[p y]") as "own_p_q". { iFrame. }
-    iMod (own_sep_inv_incll_nondet γ (p1 ⋅ q) state0.1 state0.2 (λ p2_q r , ∃ p2 b2 t2 , p2_q = p2 ⋅ q /\ output_ok p2 b2
-          /\ interp_rel ((p2 ⋅ q) ⋅ r) t2
-          /\ ✓(state0.2 ⋅ b1)
-          /\ state0.2 ⋅ b1 ≡ t2 ⋅ b2) with "[own_p_q x]")
-          as (z p2_q) "[%incll [own_p_q x]]".
-      { unfold storage_protocol_exchange_nondeterministic in exchng.
-        intro r. intro j0. have exq := exchng r state0.2 j0.
-        destruct exq as [p2_q [b2 [t2 exq]]].
-        destruct exq as [[p2 [eq oo]] [a b]].
-        exists (p2 ⋅ q). exists t2. split.
-        { exists p2. exists b2. exists t2. intuition. rewrite <- eq. apply a. }
-        { rewrite <- eq. apply a. }
-      }
-    { trivial. }
-    { iFrame. }
-      
-    destruct incll as [[p2 [b2 [t2 [p2_q_eq bigconj]]]] incll].
-    rewrite p2_q_eq.
-    iDestruct (own_inved_op_split with "own_p_q") as "[p q]".
-    iDestruct ("z" with "q") as "[_ z]".
-
-    destruct bigconj as [oo [pix [iix interp_eq]]].
-       
-    destruct wfm as [f_prop [f_unit f_op]]. (* need f Proper for the next step *)
-    
-    (*
-    assert (f (interp state0)
-          ≡ f(interp (p1 ⋅ q ⋅ z))) as equiv_interp_state.
-    {
-        setoid_rewrite incll. trivial.
-    }*)
-    
-    iDestruct "z" as "[g [_ fi]]".
-    (*setoid_rewrite equiv_interp_state.*)
-    iDestruct (bi.later_sep with "[fi f]") as "f_op". { iFrame "fi". iFrame "f". }
-    
-    unfold storage_protocol_exchange in exchng.
-    assert (pinv (p1 ⋅ q ⋅ z)) as pinv_p1_z. {
-        destruct storage_mixin. destruct protocol_mixin0.
-        setoid_rewrite <- incll. rewrite p_inv_equiv; trivial. exists (state0.2).
-        apply pinvs.
-    }
-
-    assert (✓ (t2 ⋅ b2)) as val_interp2.
-    {
-      destruct storage_mixin. destruct base_ra_mixin0.
-      setoid_rewrite <- interp_eq. trivial.
-    }
-    
-    setoid_rewrite <- f_op; trivial.
-
-    setoid_rewrite interp_eq.
-    setoid_rewrite f_op; trivial.
-    
-    iDestruct "f_op" as "[fi fb]".
-
-    iAssert ((▷ ∃ state0_t : P * B,
-          own γ (● Inved state0_t.1) ∗ ⌜interp_rel state0_t.1 state0_t.2⌝ ∗ f state0_t.2)%I)
-          with "[x fi]"
-          as "inv_to_return".
-    {
-      iModIntro.
-      iExists (p2 ⋅ q ⋅ z, t2). iFrame "x". iFrame "fi".
-      iPureIntro. trivial.
-    }
-    iDestruct ("g" with "inv_to_return") as "g".
-    iMod ("back" with "g") as "g".
-    iModIntro. iFrame. iPureIntro. trivial.
-  Qed.
-  
-  Lemma logic_exchange_with_extra_guard_nondeterministic
-    (p1 q: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ) E
-    (exchng: storage_protocol_exchange_nondeterministic (p1 ⋅ q) b1
-        (λ p2_q b2 , ∃ p2 , p2_q = p2 ⋅ q /\ output_ok p2 b2))
-    (gname_in_e: γ ∈ E)
-    : maps γ f ∗ (G &&{ E }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ E }=∗ ∃ p2 b2 ,
-            ⌜ output_ok p2 b2 ⌝ ∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H10 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "x y".
-    iDestruct (logic_exchange_with_extra_guard_nondeterministic_with_later p1 q b1 output_ok γ f G E 0 exchng gname_in_e with "x y") as "J".
-    iMod "J". iMod "J". iModIntro. iFrame.
-  Qed.
-  
-  Lemma logic_exchange_with_extra_guard
-    (p1 p2 q: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ) (G: iProp Σ)
-    (exchng: storage_protocol_exchange (p1 ⋅ q) (p2 ⋅ q) b1 b2)
-    : maps γ f ∗ (G &&{ {[ γ ]} }&&> p_own γ q) ⊢
-        G ∗ p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ G ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "x y".
-    iDestruct (logic_exchange_with_extra_guard_nondeterministic p1 q b1 (λ p b, p = p2 ∧ b = b2) γ f G {[ γ ]} with "x y") as "J".
-    { unfold storage_protocol_exchange_nondeterministic.
-      unfold storage_protocol_exchange in exchng.
-      intros q0 t1 pi. exists (p2 ⋅ q). exists b2. have ex := exchng q0 t1 pi.
-      destruct ex as [t2 ex]. exists t2.
-      split. { exists p2. split; trivial. split; trivial. }
-      apply ex.
-    }
-    { set_solver. }
-    iMod "J" as (p0 b0) "[[%es %es2] L]". iModIntro. subst p0. subst b0. iFrame.
-  Qed.
-  
-  (*
-  Lemma logic_exchange_nondeterministic
-    (p1: P) (b1: B) (output_ok: P -> B -> Prop) (γ: gname) (f: B -> iProp Σ)
-    (exchng: storage_protocol_exchange_nondeterministic p1 b1 output_ok)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗
-          ∃ p2 b2 , ⌜ output_ok p2 b2 ⌝ ∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "maps p_own".
-    iDestruct (logic_exchange_with_extra_guard_nondeterministic p1 ε b1 output_ok γ f True {[ γ ]}) as "J".
-    { unfold storage_protocol_exchange_nondeterministic in *. intros q pi.
-      assert (p1 ⋅ ε ≡ p1) as X. {
-        destruct storage_mixin. destruct protocol_mixin.
-        rewrite ra_comm; trivial.
-      }
-      assert (pinv (p1 ⋅ q)) as Y. {
-        destruct storage_mixin. destruct protocol_mixin.
-          apply inv_proper with (x := (p1 ⋅ ε) ⋅ q); trivial.
-          rewrite ra_comm; trivial.
-          setoid_replace (p1 ⋅ q) with (q ⋅ p1) by (rewrite ra_comm; trivial).
-          have op_proper := (ra_op_proper P protocol_ra_mixin).
-          unfold Proper, "==>", impl in op_proper.
-          have opp := op_proper q (p1 ⋅ ε) p1.
-          apply opp. apply X.
-      }
-      
-      have ex := exchng q Y.
-      destruct ex as [p2 [b2 [oo [pi2 in2]]]].
-      exists (p2 ⋅ ε). exists b2.
-      
-      assert (p2 ⋅ ε ≡ p2) as Z. {
-        destruct storage_mixin. destruct protocol_mixin.
-        rewrite ra_comm; trivial.
-      }
-      assert (pinv (p2 ⋅ ε ⋅ q)) as W. {
-        destruct storage_mixin. destruct protocol_mixin.
-          apply inv_proper with (x := (p2 ⋅ q)); trivial.
-          rewrite ra_comm; trivial.
-          setoid_replace (p2 ⋅ ε ⋅ q) with (q ⋅ (p2 ⋅ ε)) by (rewrite ra_comm; trivial).
-          have op_proper := (ra_op_proper P protocol_ra_mixin).
-          unfold Proper, "==>", impl in op_proper.
-          have opp := op_proper q p2 (p2 ⋅ ε).
-          apply opp. symmetry. apply Z.
-      }
-      intuition.
-      { exists p2. split; trivial. }
-   *)   
-
-    
-  
-  Lemma inved_op (a b : P) :
-      Inved (a ⋅ b) ≡ Inved a ⋅ Inved b.
-  Proof using H4 H6 H7 P equ. trivial. Qed.
-
-  (* SP-Sep *)
-
-  Lemma p_own_op a b γ :
-      p_own γ (a ⋅ b) ⊣⊢ p_own γ a ∗ p_own γ b.
-  Proof.
-    unfold p_own.
-    setoid_rewrite inved_op.
-    rewrite auth_frag_op.
-    apply own_op.
-  Qed.
-  
-  Lemma op_unit (p: P) : p ⋅ ε ≡ p.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct protocol_mixin.
-    destruct protocol_ra_mixin.
-    setoid_rewrite (@comm P).
-    - apply protocol_unit_left_id.
-    - trivial.
-  Qed.
-  
-  Lemma op_unit_base (b: B) : b ⋅ ε ≡ b.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct base_ra_mixin0.
-    setoid_rewrite (@comm B).
-    - apply base_unit_left_id0.
-    - trivial.
-  Qed.
-  
-  Lemma auth_inved_conjure_unit γ (state: P)
-      : own γ (● Inved state) ==∗ own γ (● Inved state) ∗ own γ (◯ Inved ε).
-  Proof.
-      apply auth_conjure_frag.
-      setoid_rewrite <- inved_op.
-      setoid_rewrite op_unit.
-      trivial.
-  Qed.
-
-  (* SP-Unit *)
-  
-  Lemma p_own_unit γ f
-      : maps γ f ⊢ p_own γ ε.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    unfold maps.
-    iIntros "[%wfm [#ounit #m]]".
-    unfold p_own.
-    iFrame "ounit".
-  Qed.
-
-  (* SP-Deposit *)
-    
-  Lemma logic_deposit
-      (p1 p2: P) (b1: B) (γ: gname) (f: B -> iProp Σ)
-      (exchng: storage_protocol_deposit p1 p2 b1)
-      : maps γ f ⊢
-          p_own γ p1 ∗ ▷ f b1 ={ {[ γ ]} }=∗ p_own γ p2.
-   Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "#m pb".
-    iMod (logic_exchange p1 p2 b1 (ε: B) γ f with "m pb") as "[pb u]".
-    {
-      unfold storage_protocol_exchange.
-      unfold storage_protocol_deposit in exchng.
-      intros q pi1. have t := exchng q pi1. intuition.
-      setoid_rewrite op_unit_base.
-      trivial.
-    }
-    iModIntro. iFrame "pb".
-   Qed.
-   
-  Instance valid_proper_base : Proper ((≡) ==> impl) (@valid B _).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct base_ra_mixin0.
-    apply ra_validN_proper.
-  Qed.
-  
-  Instance pinv_proper : Proper ((≡) ==> impl) (@pinv P _).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    destruct protocol_mixin0.
-    apply inv_proper.
-  Qed.
-  
-  (*Lemma valid_interp (p: P)
-      : pinv p -> ✓ (interp p).
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    destruct storage_mixin.
-    apply interp_val0.
-  Qed.*)
-
-  (* SP-Withdraw *)
-   
-  Lemma logic_withdraw
-      (p1 p2: P) (b2: B) (γ: gname) (f: B -> iProp Σ)
-      (exchng: storage_protocol_withdraw p1 p2 b2)
-      : maps γ f ⊢
-          p_own γ p1 ={ {[ γ ]} }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "#m pb".
-    iAssert (▷ f ε)%I as "u".
-    {
-      iModIntro. 
-      unfold maps.
-      iDestruct "m" as "[%wf #m]".
-      unfold wf_prop_map in wf.
-      destruct wf as [wf_prop [wf_unit _]].
-      setoid_rewrite wf_unit. done.
-    }
-    iMod (logic_exchange p1 p2 (ε: B) b2 γ f with "m [pb u]") as "[pb fb2]".
-    {
-      unfold storage_protocol_exchange.
-      unfold storage_protocol_withdraw in exchng.
-      intros q t1 pi1. have j := exchng q t1 pi1. destruct j as [t2 j].
-      exists t2. intuition.
-      - setoid_rewrite op_unit_base.
-        destruct storage_mixin. apply (interp_val0 (p1 ⋅ q)). trivial.
-      - setoid_rewrite op_unit_base. trivial.
-    }
-    { iFrame "pb". iFrame "u". }
-    iModIntro. iFrame.
-   Qed.
-
-  (* SP-Update *)
-   
-  Lemma logic_update
-      (p1 p2: P) (γ: gname) (f: B -> iProp Σ)
-      (exchng: storage_protocol_update p1 p2)
-      : maps γ f ⊢
-          p_own γ p1 ={ {[ γ ]} }=∗ p_own γ p2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "#m pb".
-    iDestruct (logic_withdraw p1 p2 ε γ f with "m pb") as "pb".
-    {
-      unfold storage_protocol_withdraw.
-      unfold storage_protocol_update in exchng.
-      intros q t1 pi.
-      have exch := exchng q t1.
-      intuition.
-      setoid_rewrite op_unit_base. exists t1. split; trivial.
-    }
-    iMod "pb".
-    iModIntro.
-    iDestruct "pb" as "[pb _]".
-    iFrame.
-  Qed.
-  
-  Lemma valid_inved_of_pinv (p: P)
-    : pinv p -> ✓ (Inved p). 
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ inG0 storage_mixin Σ.
-    intro pi. unfold "✓", inved_protocol_valid. exists ε. setoid_rewrite op_unit.
-    trivial.
-  Qed.
-
-  (* SP-Alloc *)
-  
-  Lemma logic_init_ns (p: P) (b: B) (f: B -> iProp Σ) E (N: namespace)
-      (pi: interp_rel p b) (wf: wf_prop_map f)
-  : ⊢ f b ={E}=∗ ∃ γ , ⌜ γ ∈ (↑ N : coPset) ⌝ ∗ maps γ f ∗ p_own γ p.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "f_init".
-    rewrite fancy_updates.uPred_fupd_unseal. unfold fancy_updates.uPred_fupd_def.
-    iIntros "[w oe]".
-    iMod (ownI_alloc_and_simultaneous_own_alloc_ns
-      (λ γ , 
-        (∃ (state_t: P * B) ,
-          own γ (● (Inved state_t.1))
-          ∗ ⌜ interp_rel state_t.1 state_t.2 ⌝
-          ∗ (f state_t.2))%I
-      )
-      (● (Inved p) ⋅ (◯ (Inved ε) ⋅ ◯ (Inved p)))
-      (↑ N)
-      with "w") as "w".
-    { rewrite coPset_infinite_finite. apply nclose_infinite. }
-    { 
-      rewrite <- auth_frag_op.
-      rewrite auth_both_valid_discrete. split; trivial.
-      - replace (Inved ε ⋅ Inved p) with (Inved (ε ⋅ p)) by trivial.
-        destruct storage_mixin. destruct protocol_mixin0. rewrite protocol_unit_left_id.
-        trivial.
-      - apply valid_inved_of_pinv. rewrite p_inv_equiv; trivial. exists b. apply pi.
-    }
-    
-    iDestruct "w" as (γ) "[%in_ns [w [oinv [auth [u frag]]]]]".
-    
-    iDestruct ("w" with "[auth f_init]") as "w".
-    {
-      iModIntro. iExists (p, b). iFrame. iPureIntro. trivial.
-    }
-    
-    iModIntro. iModIntro.
-    iFrame "w". iFrame "oe".
-    iExists γ.
-    unfold p_own. iFrame "frag".
-    unfold maps.
-    iFrame "oinv". iFrame.
-    iPureIntro. split; trivial.
-  Qed.
-  
-  Lemma logic_init (p: P) (b: B) (f: B -> iProp Σ) E
-      (pi: interp_rel p b) (wf: wf_prop_map f)
-  : ⊢ f b ={E}=∗ ∃ γ , maps γ f ∗ p_own γ p.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    iIntros "f_init".
-    iMod (logic_init_ns p b f E nroot with "f_init") as (γ) "[_ t]"; trivial.
-    iModIntro. iExists γ. iFrame.
-  Qed.
-  
-  Lemma fupd_singleton_mask_frame (γ: gname) (X Y Z : iProp Σ) E
-    (premise: X ⊢ Y ={ {[ γ ]} }=∗ Z) (is_in: γ ∈ E) : X ⊢ Y ={ E }=∗ Z.
-  Proof using B H equb invGS0 Σ.
-    iIntros "x y".
-    iDestruct (premise with "x y") as "p".
-    iDestruct (fupd_mask_frame_r _ _ (E ∖ {[γ]}) with "p") as "p".
-    { set_solver. }
-    assert ({[γ]} ∪ E ∖ {[γ]} = E) as sete. {
-        replace ({[γ]} ∪ E ∖ {[γ]}) with ((E ∖ {[γ]}) ∪ {[γ]}) by set_solver.
-        apply guarding.guard.elem_diff_union_singleton. trivial.
-    }
-    rewrite sete. 
-    trivial.
-  Qed.
-    
-  Lemma logic_exchange'
-    (p1 p2: P) (b1 b2: B) (γ: gname) (f: B -> iProp Σ) E
-    (exchng: storage_protocol_exchange p1 p2 b1 b2)
-    (gname_in_e: γ ∈ E)
-    : maps γ f ⊢
-        p_own γ p1 ∗ ▷ f b1 ={ E }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_exchange; trivial.
-  Qed.
-   
-  Lemma logic_deposit'
-      (p1 p2: P) (b1: B) (γ: gname) (f: B -> iProp Σ) E
-      (exchng: storage_protocol_deposit p1 p2 b1)
-      (gname_in_e: γ ∈ E)
-      : maps γ f ⊢
-          p_own γ p1 ∗ ▷ f b1 ={ E }=∗ p_own γ p2.
-   Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_deposit; trivial.
-   Qed.
-
-  Lemma logic_withdraw'
-      (p1 p2: P) (b2: B) (γ: gname) (f: B -> iProp Σ) E
-      (exchng: storage_protocol_withdraw p1 p2 b2)
-      (gname_in_e: γ ∈ E)
-      : maps γ f ⊢
-          p_own γ p1 ={ E }=∗ p_own γ p2 ∗ ▷ f b2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_withdraw; trivial.
-  Qed.
-
-  Lemma logic_update'
-      (p1 p2: P) (γ: gname) (f: B -> iProp Σ) E
-      (exchng: storage_protocol_update p1 p2)
-      (gname_in_e: γ ∈ E)
-      : maps γ f ⊢
-          p_own γ p1 ={ E }=∗ p_own γ p2.
-  Proof using B H H0 H1 H2 H3 H4 H5 H6 H7 H8 H9 P equ equb inG0 invGS0 storage_mixin Σ.
-    apply (fupd_singleton_mask_frame γ); trivial.
-    apply logic_update; trivial.
-  Qed.
-  
-  (* SP-PointProp *)
-  
-  Lemma point_prop_p_own (γ: gname) (p: P) : point_prop (p_own γ p).
-  Proof.
-    unfold p_own. apply point_prop_own.
-  Qed.
-  
-  (* SP-Valid *)
-  
-  Lemma p_own_valid (γ: gname) (p: P)
-      : (p_own γ p) ⊢ ⌜ ∃ q , pinv (p ⋅ q) ⌝.
-  Proof.
-    iIntros "x".  iDestruct (own_valid with "x") as "%x". iPureIntro.
-    generalize x. clear x.
-    rewrite auth_frag_valid.
-    trivial.
-  Qed.
- 
-End StorageLogic.