WIP

theories/auth_excl.v

@@ -21,6 +21,27 @@ Proof. (* TODO: RK fix this *) Admitted.
 
 Definition to_auth_excl {A : ofeT} (a : A) : exclUR A :=
   Excl' a.
+Instance: Params (@to_auth_excl) 1.
+
+Section auth_excl_ofe.
+  Context {A : ofeT}.
+  
+  Global Instance to_auth_excl_ne : NonExpansive (@to_auth_excl A).
+  Proof.
+    intros n.
+    intros x y Heq.
+    rewrite /to_auth_excl.
+    by repeat f_equiv.
+  Qed.
+
+  Global Instance to_auth_excl_proper :
+    Proper ((≡) ==> (≡)) (@to_auth_excl A).
+  Proof.
+    intros x y Heq.
+    rewrite /to_auth_excl.
+    by repeat f_equiv.
+  Qed.
+End auth_excl_ofe.
 
 Section auth_excl.
   Context `{!auth_exclG A Σ}.

theories/logrel.v

@@ -7,15 +7,17 @@ From osiris Require Import typing auth_excl channel.
 From iris.algebra Require Import list auth excl.
 From iris.base_logic Require Import invariants.
 
+
 Class logrelG Σ := {
-  logrelG_channelG : chanG Σ;
-  logrelG_authG : auth_exclG (stype (later (iProp Σ))) Σ;
+  logrelG_channelG :> chanG Σ;
+  logrelG_authG :> auth_exclG (@stypeC (laterC (iProp Σ))) Σ; (* Annotation? *)
 }.
 
 Section logrel.
   Context `{!heapG Σ, !lockG Σ} (N : namespace).
-  Context `{!auth_exclG (list val) Σ}.
-  Context `{!auth_exclG stype Σ}.
+  Context `{!logrelG Σ}.
+
+  Notation stype_iprop := (@stypeC (laterC (iProp Σ))).
 
   Record st_name := SessionType_name {
     st_c_name : chan_name;
@@ -23,20 +25,20 @@ Section logrel.
     st_r_name : gname
   }.
 
-  Definition st_own (γ : st_name) (s : side) (st : stype) : iProp Σ :=
+  Definition st_own (γ : st_name) (s : side) (st : stype_iprop)  : iProp Σ :=
     own (side_elim s st_l_name st_r_name γ) (◯ to_auth_excl st)%I.
-
-  Definition st_ctx (γ : st_name) (s : side) (st : stype) : iProp Σ :=
+  
+  Definition st_ctx (γ : st_name) (s : side) (st : stype_iprop) : iProp Σ :=
     own (side_elim s st_l_name st_r_name γ) (● to_auth_excl st)%I.
 
-  Fixpoint st_eval (vs : list val) (st1 st2 : stype) : Prop :=
+  Fixpoint st_eval (vs : list val) (st1 st2 : stype_iprop) : iProp Σ :=
     match vs with
-    | [] => st1 = dual_stype st2
+    | [] => st1 ≡ dual_stype st2
     | v::vs => match st2 with
-               | TRecv P st2 => P v ∧ st_eval vs st1 (st2 v)
+               | TSR Receive P st2 => ▷ P v ∗ st_eval vs st1 (st2 v)
                | _ => False
                end
-    end.
+    end%I.
 
   Lemma st_eval_send (P : val -> Prop) st l str v :
       P v → st_eval l (TSend P st) str → st_eval (l ++ [v]) (st v) str.