Introduced encoding for branching

_CoqProject

@@ -8,6 +8,9 @@ theories/encodings/auth_excl.v
 theories/encodings/channel.v
 theories/encodings/stype.v
 theories/encodings/stype_enc.v
+theories/encodings/branching.v
 theories/examples/examples.v
 theories/examples/proofs.v
 theories/examples/proofs_enc.v
+theories/examples/branching_examples.v
+theories/examples/branching_proofs.v

theories/encodings/branching.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Import proofmode notation.
+From iris.algebra Require Import list auth excl.
+From iris.base_logic Require Import invariants.
+From osiris.encodings Require Export stype_enc.
+
+Section DualBranch.
+  Context `{PROP : bi}.
+
+  Definition TSB (a : action)
+             (st1 st2 : stype val PROP) : stype val PROP :=
+    TSR' a (λ _, True)%I (λ v, if v : bool then st1 else st2).
+
+  Global Instance is_dual_tsb a1 a2 st1 st1' st2 st2' :
+    IsDualAction a1 a2 →
+    IsDualStype st1 st1' → IsDualStype st2 st2' →
+    IsDualStype (TSB a1 st1 st2) (TSB a2 st1' st2').
+  Proof.
+    rewrite /IsDualAction.
+    rewrite /IsDualStype.
+    intros Ha Hst1 Hst2.
+    destruct a1.
+    - simpl.
+      simpl in Ha. rewrite Ha.
+      constructor.
+      f_equiv.
+      f_equiv.
+      destruct (decode a).
+      by destruct b. done.
+    - simpl.
+      simpl in Ha. rewrite Ha.
+      constructor.
+      f_equiv.
+      f_equiv.
+      destruct (decode a).
+        by destruct b.
+        done.
+  Qed.
+End DualBranch.
+Global Typeclasses Opaque TSB.
+
+Notation TSelect := (TSB Send).
+Notation TBranch := (TSB Receive).
+
+Section branching_specs.
+  Context `{!heapG Σ} (N : namespace).
+  Context `{!logrelG val Σ}.
+
+  Definition select : val :=
+    λ: "c" "s" "b",
+      send "c" "s" "b".
+
+  Definition branch : val :=
+    λ: "c" "s" "b1" "b2",
+      if: recv "c" "s"
+      then "b1"
+      else "b2".
+
+  Lemma select_st_spec st1 st2 γ c s (b : bool) :
+    {{{ ⟦ c @ s : TSelect st1 st2 ⟧{N,γ} }}}
+      select c #s #b
+    {{{ RET #(); ⟦ c @ s : (if b then st1 else st2) ⟧{N,γ} }}}.
+  Proof.
+    iIntros (Φ) "Hst HΦ".
+    wp_pures. wp_lam.
+    wp_pures. rewrite /TSB.
+    wp_apply (send_st_spec N bool with "[$Hst //]");
+    iIntros "Hstl".
+    iApply "HΦ".
+    eauto.
+  Qed.
+
+  Lemma branch_st_spec st1 st2 γ c s (b1 b2 : val) Φ :
+    ⟦ c @ s : TBranch st1 st2 ⟧{N,γ} -∗
+    (⟦ c @ s : st1 ⟧{N,γ} -∗ (Φ b1)) -∗
+    (⟦ c @ s : st2 ⟧{N,γ} -∗ (Φ b2)) -∗
+    WP branch c #s b1 b2 {{ v, Φ v }}.
+  Proof.
+    iIntros "Hst Hb1 Hb2".
+    wp_lam. rewrite /TSB.
+    wp_apply (recv_st_spec N bool with "[$Hst //]").
+    iIntros (v) "[Hstl _]".
+    destruct v; wp_pures.
+    - by iApply "Hb1".
+    - by iApply "Hb2".
+  Qed.
+
+End branching_specs.
\ No newline at end of file

theories/examples/branching_examples.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Import proofmode notation.
+From osiris.typing Require Import side stype.
+From osiris.encodings Require Import channel branching.
+From iris.base_logic Require Import invariants.
+
+Section BranchingExamples.
+  Context `{!heapG Σ} (N : namespace).
+
+  Definition branch_example b : expr :=
+    (let: "c" := new_chan #() in
+     select "c" #Left #b;;
+     Fork((branch "c" #Right
+      (λ: <>, send "c" #Right #5)
+      (λ: <>, #())) #());;
+     (if: #b then recv "c" #Left else #()))%E.
+
+End BranchingExamples.
\ No newline at end of file

theories/examples/branching_proofs.v

+From iris.proofmode Require Import tactics.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Import proofmode notation.
+From iris.base_logic Require Import invariants.
+From osiris.typing Require Import side stype.
+From osiris.encodings Require Import branching.
+From osiris.examples Require Import branching_examples.
+
+Section BranchingExampleProofs.
+  Context `{!heapG Σ} (N : namespace).
+  Context `{!logrelG val Σ}.
+
+  Lemma branch_proof b :
+    {{{ True }}}
+      branch_example b
+    {{{ v, RET v; match b with
+                  | true => ⌜v = #5⌝
+                  | false => ⌜v = #()⌝
+                  end }}}.
+  Proof.
+    iIntros (Φ H) "HΦ".
+    rewrite /branch_example.
+    wp_apply (new_chan_st_spec N (TSelect
+                                    (TReceive (λ v, ⌜v = 5⌝%I) (λ v, TEnd))
+                                    TEnd))=> //;
+    iIntros (c γ) "[Hstl Hstr]".
+    wp_apply (select_st_spec with "Hstl");
+    iIntros "Hstl".
+    wp_pures.
+    wp_apply (wp_fork with "[Hstr]").
+    - iNext.
+      wp_apply (branch_st_spec N with "Hstr");
+      iIntros "Hstr".
+      + wp_apply (send_st_spec N Z with "[$Hstr //]");
+        iIntros "Hstr". done.
+      + wp_pures. done.
+    - destruct b.
+      + wp_apply (recv_st_spec N Z with "Hstl");
+        iIntros (v) "[Hstl HP]".
+        iDestruct "HP" as %->.
+        by iApply "HΦ".
+      + wp_pures. by iApply "HΦ".
+  Qed.
+
+End BranchingExampleProofs.
\ No newline at end of file