Improved stype encoding layer and added automatic dual rewrites

theories/encodings/stype.v

@@ -20,7 +20,7 @@ Definition logrelΣ A :=
 Instance subG_chanΣ {A Σ} : subG (logrelΣ A) Σ → logrelG A Σ.
 Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
 
-Section logrel.
+Section stype_interp.
   Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
@@ -148,6 +148,22 @@ Section logrel.
       (c : val) (s : side) : iProp Σ :=
     (st_own γ s st ∗ is_st γ st c)%I.
 
+  Global Instance interp_st_proper γ : Proper ((≡) ==> (=) ==> (=) ==> (≡)) (interp_st γ).
+  Proof.
+    intros st1 st2 Heq v1 v2 <- s1 s2 <-.
+    iSplit;
+    iIntros "[Hown Hctx]";
+    iFrame;
+    unfold st_own;
+    iApply (own_mono with "Hown");
+    apply (auth_frag_mono);
+    apply Some_included;
+    left;
+    f_equiv;
+    f_equiv;
+    apply stype_map_equiv=> //.
+  Qed.
+
   Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st γ sτ c s)
     (at level 10, s at next level, sτ at next level, γ at next level,
      format "⟦  c  @  s  :  sτ  ⟧{ γ }").
@@ -176,22 +192,25 @@ Section logrel.
     iFrame "Hlstf Hrstf Hcctx Hinv".
   Qed.
 
-  Lemma new_chan_st_spec st :
+  Lemma new_chan_st_spec st1 st2 :
+    IsDualStype st1 st2 →
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c;  ⟦ c @ Left : st ⟧{γ} ∗
-                     ⟦ c @ Right : dual_stype st ⟧{γ} }}}.
+    {{{ c γ, RET c;  ⟦ c @ Left : st1 ⟧{γ} ∗
+                     ⟦ c @ Right : st2 ⟧{γ} }}}.
   Proof.
-    iIntros (Φ _) "HΦ".
+    rewrite /IsDualStype.
+    iIntros (Hst Φ _) "HΦ".
     iApply (wp_fupd).
     iApply (new_chan_spec)=> //.
     iModIntro.
     iIntros (c γ) "[Hc Hctx]".
-    iMod (new_chan_vs st ⊤ c γ with "[-HΦ]") as "H".
+    iMod (new_chan_vs st1 ⊤ c γ with "[-HΦ]") as "H".
     { rewrite /is_chan. eauto with iFrame. }
     iDestruct "H" as (lγ rγ) "[Hl Hr]".
     iApply "HΦ".
-    by iFrame.
+    rewrite Hst.
+    by iFrame.        
   Qed.
 
   Lemma send_vs c γ s (P : val → iProp Σ) st E :
@@ -388,4 +407,4 @@ Section logrel.
       iFrame.
   Qed.
 
-End logrel.
\ No newline at end of file
+End stype_interp.
\ No newline at end of file

theories/encodings/stype_enc.v

@@ -70,35 +70,50 @@ Proof.
     apply decenc. eauto.
 Qed.
 
-Inductive stype (A : Type) :=
-| TEnd
-| TSR {V : Type} {EV : Encodable V} {DV : Decodable V}
-       (a : action) (P : V → A) (st : V → stype A).
-Arguments TEnd {_}.
-Arguments TSR {_ _ _ _} _ _ _.
-Instance: Params (@TSR) 4.
-
-Notation TSend P st := (TSR Send P st).
-Notation TReceive P st := (TSR Receive P st).
-
-Fixpoint dual_stype {A} (st : stype A) :=
-  match st with
-  | TEnd => TEnd
-  | TSR a P st => TSR (dual_action a) P (λ v, dual_stype (st v))
-  end.
-Instance: Params (@dual_stype) 2.
-Arguments dual_stype : simpl never.
+Definition TSR' `{PROP: bi} {V} `{ED : EncDec V}
+    (a : action) (P : V → PROP) (st : V → stype val PROP) : stype val PROP :=
+  TSR a
+    (λ v, if decode v is Some x then P x else False)%I
+    (λ v, if decode v is Some x then st x else TEnd (* dummy *)).
+Instance: Params (@TSR') 4.
+
+Notation TSend P st := (TSR' Send P st).
+Notation TReceive P st := (TSR' Receive P st).
+
+Section DualStypeEnc.
+  Context `{PROP: bi} `{EncDec V}.
+
+  Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V → stype val PROP) :
+    IsDualAction a1 a2 →
+    (∀ x, IsDualStype (st1 x) (st2 x)) →
+    IsDualStype (TSR' a1 P st1) (TSR' a2 P st2).
+  Proof.
+    rewrite /IsDualAction /IsDualStype. intros <- Hst.
+    constructor=> x. done. by destruct (decode x).
+  Qed.
+
+  Global Instance is_dual_send P (st1 st2 : V → stype val PROP) :
+    (∀ x, IsDualStype (st1 x) (st2 x)) →
+    IsDualStype (TSend P st1) (TReceive P st2).
+  Proof. intros Heq. by apply is_dual_tsr'. Qed.
+  
+  Global Instance is_dual_receive P (st1 st2 : V → stype val PROP) :
+    (∀ x, IsDualStype (st1 x) (st2 x)) →
+    IsDualStype (TReceive P st1) (TSend P st2).
+  Proof. intros Heq. by apply is_dual_tsr'. Qed.
+
+End DualStypeEnc.
 
 Section Encodings.
   Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
-  Example ex_st : stype (iProp Σ) :=
+  Example ex_st : stype val (iProp Σ) :=
     (TReceive
           (λ v', ⌜v' = 5⌝%I)
           (λ v', TEnd)).
 
-  Example ex_st2 : stype (iProp Σ) :=
+  Example ex_st2 : stype val (iProp Σ) :=
     TSend
          (λ b, ⌜b = true⌝%I)
          (λ b,
@@ -106,67 +121,11 @@ Section Encodings.
               (λ v', ⌜(v' > 5) = b⌝%I)
               (λ _, TEnd))).
 
-  Fixpoint lift_stype (st : stype (iProp Σ)) : stype.stype val (iProp Σ) :=
-    match st with
-    | TEnd => stype.TEnd
-    | TSR a P st =>
-      stype.TSR a
-          (λ v, match decode v with
-                | Some v => P v
-                | None => False
-                end%I)
-          (λ v, match decode v with
-                | Some v => lift_stype (st v)
-                | None => stype.TEnd
-                end)
-    end.
-  Global Instance: Params (@lift_stype) 1.
-  Global Arguments lift_stype : simpl never.
-
-  Instance stype_equiv : Equiv (stype (iProp Σ)) :=
-    λ st1  st2, lift_stype st1 ≡ lift_stype st2.
-
-  Lemma lift_dual_comm st :
-    lift_stype (dual_stype st) ≡ stype.dual_stype (lift_stype st).
-  Proof.
-    induction st.
-    - by simpl.
-    - unfold lift_stype. simpl.
-      constructor.
-      + intros v. eauto.
-      + intros v. destruct (decode v); eauto.
-  Qed.
-
-  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ (lift_stype sτ) c s)
+  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
     (at level 10, s at next level, sτ at next level, γ at next level,
      format "⟦  c  @  s  :  sτ  ⟧{ γ }").
 
-  Lemma new_chan_st_spec st :
-    {{{ True }}}
-      new_chan #()
-    {{{ c γ, RET c; ⟦ c @ Left : st ⟧{γ} ∗
-                    ⟦ c @ Right : (dual_stype st) ⟧{γ} }}}.
-  Proof.
-    iIntros (Φ _) "HΦ".
-    iApply (new_chan_st_spec). eauto.
-    iNext.
-    iIntros (c γ) "[Hl Hr]".
-    iApply "HΦ".
-    iFrame.
-    iDestruct "Hr" as "[Hown Hctx]".
-    iFrame.
-    unfold st_own. simpl.
-    iApply (own_mono with "Hown").
-    apply (auth_frag_mono).
-    apply Some_included.
-    left.
-    f_equiv.
-    f_equiv.
-    apply stype_map_equiv=> //.
-    apply lift_dual_comm.
-  Qed.
-
-  Lemma send_st_spec (A : Type) `{Encodable A} `{Decodable A} `{EncDec A}
+  Lemma send_st_spec (A : Type) `{EncDec A}
         st γ c s (P : A → iProp Σ) w :
     {{{ P w ∗ ⟦ c @ s : (TSend P st) ⟧{γ} }}}
       send c #s (encode w)

theories/examples/proofs_enc.v

@@ -10,21 +10,21 @@ Section ExampleProofsEnc.
   Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
-  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ (lift_stype sτ) c s)
+  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
     (at level 10, s at next level, sτ at next level, γ at next level,
      format "⟦  c  @  s  :  sτ  ⟧{ γ }").
-
+  
   Lemma seq_proof :
     {{{ True }}} seq_example {{{ v, RET v; ⌜v = #5⌝ }}}.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /seq_example.
     wp_apply (new_chan_st_spec N
-             (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+             (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //.
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (send_st_spec N Z with "[$Hstl //]");
     iIntros "Hstl".
-    wp_apply (recv_st_spec N Z with "Hstr");
+    wp_apply (recv_st_spec N Z with "[Hstr]"). iApply "Hstr".
     iIntros (v) "[Hstr HP]".
     iApply "HΦ".
     iDestruct "HP" as %->.    
@@ -98,7 +98,7 @@ Section ExampleProofsEnc.
     wp_apply (wp_fork with "[Hstl]").
     - iNext.
       wp_apply (new_chan_st_spec N
-        (TSR Send (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
+        (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
       iIntros (c' γ') "[Hstl' Hstr']"=> /=.
       wp_apply (send_st_spec N val with "[Hstl Hstr']");
         first by eauto 10 with iFrame.

theories/typing/stype.v

@@ -14,6 +14,15 @@ Definition dual_action (a : action) : action :=
 Instance dual_action_involutive : Involutive (=) dual_action.
 Proof. by intros []. Qed.
 
+Class IsDualAction (a1 a2 : action) :=
+  is_dual_action : dual_action a1 = a2.
+Instance is_dual_action_default : IsDualAction a (dual_action a) | 100.
+Proof. done. Qed.
+Instance is_dual_action_Send : IsDualAction Send Receive.
+Proof. done. Qed.
+Instance is_dual_action_Receive : IsDualAction Receive Send.
+Proof. done. Qed.
+
 Inductive stype (V A : Type) :=
   | TEnd
   | TSR (a : action) (P : V → A) (st : V → stype V A).
@@ -216,4 +225,38 @@ Instance stypeCF_contractive {V} F :
   cFunctorContractive F → cFunctorContractive (@stypeCF V F).
 Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_contractive.
-Qed.
\ No newline at end of file
+Qed.
+
+Class IsDualStype {V} {A : ofeT} (st1 st2 : stype V A) :=
+  is_dual_stype : dual_stype st1 ≡ st2.
+
+Section DualStype.
+  Context `{PROP: bi} {V : Type}.
+
+  Global Instance is_dual_default (st : stype V PROP) :
+    IsDualStype st (dual_stype st) | 100.
+  Proof. by rewrite /IsDualStype. Qed.
+
+  Global Instance is_dual_end : IsDualStype (TEnd : stype V PROP) TEnd.
+  Proof. constructor. Qed.
+
+  Global Instance is_dual_tsr a1 a2 P (st1 st2 : V → stype V PROP) :
+    IsDualAction a1 a2 →
+    (∀ x, IsDualStype (st1 x) (st2 x)) →
+    IsDualStype (TSR a1 P st1) (TSR a2 P st2).
+  Proof.
+    rewrite /IsDualAction /IsDualStype. intros <- Hst.
+    by constructor=> x.
+  Qed.
+  
+  Global Instance is_dual_send P (st1 st2 : V → stype V PROP) :
+    (∀ x, IsDualStype (st1 x) (st2 x)) →
+    IsDualStype (TSR Send P st1) (TSR Receive P st2).
+  Proof. intros H. by apply is_dual_tsr. Qed.
+  
+  Global Instance is_dual_receive P (st1 st2 : V → stype V PROP) :
+    (∀ x, IsDualStype (st1 x) (st2 x)) →
+    IsDualStype (TSR Receive P st1) (TSR Send P st2).
+  Proof. intros H. by apply is_dual_tsr. Qed.
+
+End DualStype.
\ No newline at end of file